Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cleljust Unicode version

Theorem cleljust 2060
 Description: When the class variables in definition df-clel 2249 are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 1622 with the class variables in wcel 1621. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (Revised by NM, 10-Jan-2017.) (Proof modification is discouraged.)
Assertion
Ref Expression
cleljust
Distinct variable groups:   ,   ,

Proof of Theorem cleljust
StepHypRef Expression
1 ax-17 1628 . . . 4
21nfi 1556 . . 3
3 elequ1 1831 . . 3
42, 3equsex 1852 . 2
54bicomi 195 1
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360  wex 1537   wceq 1619   wcel 1621 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-8 1623  ax-13 1625  ax-17 1628  ax-9 1684  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
 Copyright terms: Public domain W3C validator