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

Theorem equsexALT 2443
Description: Alternate proof of equsex 2442. This proves the result directly, instead of as a corollary of equsal 2441 via equs4 2440. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2392 is ax6e 2403. This proof mimics that of equsal 2441 (in particular, note that pm5.32i 578, exbii 1849, 19.41 2239, mpbiran 708 correspond respectively to pm5.74i 274, albii 1821, 19.23 2213, a1bi 366). (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 578 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
32exbii 1849 . 2 (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝑦𝜓))
4 ax6e 2403 . . 3 𝑥 𝑥 = 𝑦
5 equsal.1 . . . 4 𝑥𝜓
6519.41 2239 . . 3 (∃𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
74, 6mpbiran 708 . 2 (∃𝑥(𝑥 = 𝑦𝜓) ↔ 𝜓)
83, 7bitri 278 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2179  ax-13 2392
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator