Theorem equsex 2416

Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See equsexvw 2005 and equsexv 2269 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2415. See equsexALT 2417 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 2218	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓)
5	1, 2	equsal 2415	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
6		equs4 2414	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	sylbir 235	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
8	4, 7	impbii 209	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178  ax-13 2370

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784

This theorem is referenced by:  equsexh  2419  sb5rf  2465