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

Theorem cleljust 1954
Description: When the class variables in definition df-clel 2279 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 1685 with the class variables in wcel 1684. 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-17 1603 . . 3  |-  ( x  e.  y  ->  A. z  x  e.  y )
2 elequ1 1687 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
31, 2equsexh 1903 . 2  |-  ( E. z ( z  =  x  /\  z  e.  y )  <->  x  e.  y )
43bicomi 193 1  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator