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

Theorem cleljust 2163
Description: When the class variables in definition df-clel 2424 are replaced with setvar 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 setvar variables in wel 1871 with the class variables in wcel 1870. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (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-5 1751 . . 3  |-  ( x  e.  y  ->  A. z  x  e.  y )
2 elequ1 1873 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
31, 2equsexh 2095 . 2  |-  ( E. z ( z  =  x  /\  z  e.  y )  <->  x  e.  y )
43bicomi 205 1  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-10 1889  ax-12 1907  ax-13 2055
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator