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

Theorem cleljust 2063
Description: When the class variables in definition df-clel 2252 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  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Distinct variable groups:    x, z    y, z

Proof of Theorem cleljust
StepHypRef Expression
1 ax-17 1628 . . . 4  |-  ( x  e.  y  ->  A. z  x  e.  y )
21nfi 1556 . . 3  |-  F/ z  x  e.  y
3 elequ1 1831 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
42, 3equsex 1853 . 2  |-  ( E. z ( z  =  x  /\  z  e.  y )  <->  x  e.  y )
54bicomi 195 1  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537    = wceq 1619    e. 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