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

Theorem equsexALT 2329
Description: Alternate proof of equsex 2328. This proves the result directly, instead of as a corollary of equsal 2327 via equs4 2326. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2282 is ax6e 2286. This proof mimics that of equsal 2327 (in particular, note that pm5.32i 670, exbii 1814, 19.41 2141, mpbiran 973 correspond respectively to pm5.74i 260, albii 1787, 19.23 2118, a1bi 351). (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 670 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
32exbii 1814 . 2 (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝑦𝜓))
4 ax6e 2286 . . 3 𝑥 𝑥 = 𝑦
5 equsal.1 . . . 4 𝑥𝜓
6519.41 2141 . . 3 (∃𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
74, 6mpbiran 973 . 2 (∃𝑥(𝑥 = 𝑦𝜓) ↔ 𝜓)
83, 7bitri 264 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wex 1744  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator