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

Theorem equsexALT 2426
 Description: Alternate proof of equsex 2425. This proves the result directly, instead of as a corollary of equsal 2424 via equs4 2423. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2377 is ax6e 2390. This proof mimics that of equsal 2424 (in particular, note that pm5.32i 571, exbii 1944, 19.41 2270, mpbiran 701 correspond respectively to pm5.74i 263, albii 1915, 19.23 2246, a1bi 354). (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 571 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
32exbii 1944 . 2 (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝑦𝜓))
4 ax6e 2390 . . 3 𝑥 𝑥 = 𝑦
5 equsal.1 . . . 4 𝑥𝜓
6519.41 2270 . . 3 (∃𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
74, 6mpbiran 701 . 2 (∃𝑥(𝑥 = 𝑦𝜓) ↔ 𝜓)
83, 7bitri 267 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385  ∃wex 1875  Ⅎwnf 1879 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-12 2213  ax-13 2377 This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-nf 1880 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator