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

Theorem cleljustALT 2102
Description: Alternate proof of cleljust 1912. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how DV conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
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 ax-5 1766 . . 3  |-  ( x  e.  y  ->  A. z  x  e.  y )
2 elequ1 1911 . . 3  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
31, 2equsexhv 2086 . 2  |-  ( E. z ( z  =  x  /\  z  e.  y )  <->  x  e.  y )
43bicomi 207 1  |-  ( x  e.  y  <->  E. z
( z  =  x  /\  z  e.  y ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-10 1932  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator