Theorem ceqsrexv 3597

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)

Hypothesis

Ref	Expression
ceqsrexv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ceqsrexv	⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsrexv

Step	Hyp	Ref	Expression
1		df-rex 3112	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
2		an12 644	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
3	2	exbii 1849	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 281	. 2 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5		eleq1 2877	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		ceqsrexv.1	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	7	ceqsexgv 3595	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	8	bianabs 545	. 2 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ 𝜓))
10	4, 9	syl5bb 286	1 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-rex 3112

This theorem is referenced by:  ceqsrexbv  3598  ceqsrex2v  3599  reuxfrd  3687  f1oiso  7083  creur  11619  creui  11620  deg1ldg  24693  ulm2  24980  iscgra1  26604  reuxfrdf  30262  poimirlem24  35081  eqlkr3  36397  diclspsn  38490  rmxdiophlem  39956  expdiophlem1  39962  expdiophlem2  39963