Theorem equsex 2447

Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2401. See equsexvw 2037 and equsexv 2302 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2446. See equsexALT 2448 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 482	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓)
4	1, 3	exlimi 2253	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓)
5	1, 2	equsal 2446	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
6		equs4 2445	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	sylbir 238	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
8	4, 7	impbii 212	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816

This theorem is used by:  equsexh  2450  sb5rf  2496