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

Theorem equsex 2421
Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2375. See equsexvw 2002 and equsexv 2266 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2420. See equsexALT 2422 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.) (New usage is discouraged.)
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 476 . . 3 ((𝑥 = 𝑦𝜑) → 𝜓)
41, 3exlimi 2215 . 2 (∃𝑥(𝑥 = 𝑦𝜑) → 𝜓)
51, 2equsal 2420 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
6 equs4 2419 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6sylbir 235 . 2 (𝜓 → ∃𝑥(𝑥 = 𝑦𝜑))
84, 7impbii 209 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  wex 1776  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175  ax-13 2375
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781
This theorem is referenced by:  equsexh  2424  sb5rf  2470
  Copyright terms: Public domain W3C validator