MPE Home 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