Theorem ceqsrexv 3624

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 3055	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
2		an12 645	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
3	2	exbii 1848	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 278	. 2 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5		eleq1 2817	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		ceqsrexv.1	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	7	ceqsexgv 3623	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	8	bianabs 541	. 2 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ 𝜓))
10	4, 9	bitrid 283	1 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

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-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055

This theorem is referenced by:  ceqsrexbv  3625  ceqsrex2v  3627  reuxfrd  3722  f1oiso  7329  creur  12187  creui  12188  deg1ldg  26004  ulm2  26301  iscgra1  28744  reuxfrdf  32427  poimirlem24  37645  eqlkr3  39101  diclspsn  41195  rmxdiophlem  43011  expdiophlem1  43017  expdiophlem2  43018