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