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

Theorem equsexALT 2417
Description: Alternate proof of equsex 2416. This proves the result directly, instead of as a corollary of equsal 2415 via equs4 2414. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2370 is ax6e 2381. This proof mimics that of equsal 2415 (in particular, note that pm5.32i 574, exbii 1849, 19.41 2227, mpbiran 706 correspond respectively to pm5.74i 270, albii 1820, 19.23 2203, a1bi 361). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
equsal.1 𝑥𝜓
equsal.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
equsexALT (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)

Proof of Theorem equsexALT
StepHypRef Expression
1 equsal.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
21pm5.32i 574 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
32exbii 1849 . 2 (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝑦𝜓))
4 ax6e 2381 . . 3 𝑥 𝑥 = 𝑦
5 equsal.1 . . . 4 𝑥𝜓
6519.41 2227 . . 3 (∃𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
74, 6mpbiran 706 . 2 (∃𝑥(𝑥 = 𝑦𝜓) ↔ 𝜓)
83, 7bitri 274 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wex 1780  wnf 1784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-12 2170  ax-13 2370
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator