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

Theorem equsex 2328
 Description: An equivalence related to implicit substitution. See equsexvw 1978 and equsexv 2147 for versions with dv conditions proved from fewer axioms. See also the dual form equsal 2327. See equsexALT 2329 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 500 . . 3 ((𝑥 = 𝑦𝜑) → 𝜓)
41, 3exlimi 2124 . 2 (∃𝑥(𝑥 = 𝑦𝜑) → 𝜓)
51, 2equsal 2327 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
6 equs4 2326 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6sylbir 225 . 2 (𝜓 → ∃𝑥(𝑥 = 𝑦𝜑))
84, 7impbii 199 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521  ∃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-or 384  df-an 385  df-ex 1745  df-nf 1750 This theorem is referenced by:  equsexh  2331  sb5rf  2450
 Copyright terms: Public domain W3C validator