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

Theorem equsexALT 2141
Description: Alternate proof of equsex 2140. This proves the result directly, instead of as a corollary of equsal 2138 via equs4 2137. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2101 is ax6e 2104. This proof mimics that of equsal 2138 (in particular, note pm5.32i 647, exbii 1728, 19.41 2061, mpbiran 934 correspond respectively to pm5.74i 253, albii 1701, 19.23 2003, a1bi 343). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
equsex.nf  |-  F/ x ps
equsex.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
equsexALT  |-  ( E. x ( x  =  y  /\  ph )  <->  ps )

Proof of Theorem equsexALT
StepHypRef Expression
1 equsex.1 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
21pm5.32i 647 . . 3  |-  ( ( x  =  y  /\  ph )  <->  ( x  =  y  /\  ps )
)
32exbii 1728 . 2  |-  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  y  /\  ps )
)
4 ax6e 2104 . . 3  |-  E. x  x  =  y
5 equsex.nf . . . 4  |-  F/ x ps
6519.41 2061 . . 3  |-  ( E. x ( x  =  y  /\  ps )  <->  ( E. x  x  =  y  /\  ps )
)
74, 6mpbiran 934 . 2  |-  ( E. x ( x  =  y  /\  ps )  <->  ps )
83, 7bitri 257 1  |-  ( E. x ( x  =  y  /\  ph )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   E.wex 1673   F/wnf 1677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator