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

Theorem equsal 2439
 Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See equsalvw 2010 and equsalv 2268 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2440. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)
Hypotheses
Ref Expression
equsal.1 𝑥𝜓
equsal.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
equsal (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)

Proof of Theorem equsal
StepHypRef Expression
1 equsal.1 . . 3 𝑥𝜓
2119.23 2211 . 2 (∀𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
3 equsal.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43pm5.74i 273 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
54albii 1820 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦𝜓))
6 ax6e 2401 . . 3 𝑥 𝑥 = 𝑦
76a1bi 365 . 2 (𝜓 ↔ (∃𝑥 𝑥 = 𝑦𝜓))
82, 5, 73bitr4i 305 1 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  ∃wex 1780  Ⅎwnf 1784 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177  ax-13 2390 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785 This theorem is referenced by:  equsex  2440  equsalh  2442  dvelimf  2470  sb6x  2487  sb6rf  2491  bj-sbievv  34180
 Copyright terms: Public domain W3C validator