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

Theorem equsex 2436
Description: An equivalence related to implicit substitution. See equsexvw 2004 and equsexv 2260 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2435. See equsexALT 2437 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 477 . . 3 ((𝑥 = 𝑦𝜑) → 𝜓)
41, 3exlimi 2208 . 2 (∃𝑥(𝑥 = 𝑦𝜑) → 𝜓)
51, 2equsal 2435 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
6 equs4 2434 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6sylbir 236 . 2 (𝜓 → ∃𝑥(𝑥 = 𝑦𝜑))
84, 7impbii 210 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1528  wex 1773  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2167  ax-13 2385
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778
This theorem is referenced by:  equsexh  2439  sb5rf  2487
  Copyright terms: Public domain W3C validator