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

Theorem equsex 2438
 Description: An equivalence related to implicit substitution. See equsexvw 2111 and equsexv 2301 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2437. See equsexALT 2439 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.)
Hypotheses
Ref Expression
equsal.1 𝑥𝜓
equsal.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
equsex (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)

Proof of Theorem equsex
StepHypRef Expression
1 equsal.1 . . 3 𝑥𝜓
2 equsal.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32biimpa 470 . . 3 ((𝑥 = 𝑦𝜑) → 𝜓)
41, 3exlimi 2262 . 2 (∃𝑥(𝑥 = 𝑦𝜑) → 𝜓)
51, 2equsal 2437 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
6 equs4 2436 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6sylbir 227 . 2 (𝜓 → ∃𝑥(𝑥 = 𝑦𝜑))
84, 7impbii 201 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1656  ∃wex 1880  Ⅎwnf 1884 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-12 2222  ax-13 2390 This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-nf 1885 This theorem is referenced by:  equsexh  2441  sb5rf  2553
 Copyright terms: Public domain W3C validator