Theorem equsex 2449

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1567  ∃wex 1808  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212  ax-13 2403

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-nf 1813

This theorem is used by:  equsexh  2452  sb5rf  2498