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

Theorem cleljust 2103
Description: When the class variables in definition df-clel 2432 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 1726 with the class variables in wcel 1725. 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 1626 . . 3  |-  ( x  e.  y  ->  A. z  x  e.  y )
2 elequ1 1728 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
31, 2equsexh 2004 . 2  |-  ( E. z ( z  =  x  /\  z  e.  y )  <->  x  e.  y )
43bicomi 194 1  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-6 1744  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator