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

Theorem cleljustALT 1955
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. (Contributed by NM, 28-Jan-2004.) (Revised by Mario Carneiro, 21-Dec-2016.)
Assertion
Ref Expression
cleljustALT  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Distinct variable groups:    x, z    y, z

Proof of Theorem cleljustALT
StepHypRef Expression
1 nfv 1605 . . 3  |-  F/ z  x  e.  y
2 elequ1 1687 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
31, 2equsex 1902 . 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