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 2007 and equsexv 2274 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

Step	Hyp	Ref	Expression
1		equsal.1	. . 3 ⊢ Ⅎ𝑥𝜓
2		equsal.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpa 476	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓)
4	1, 3	exlimi 2223	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓)
5	1, 2	equsal 2420	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
6		equs4 2419	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	sylbir 235	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
8	4, 7	impbii 209	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2183  ax-13 2375

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786

This theorem is referenced by:  equsexh  2424  sb5rf  2470