Theorem ceqsrexv 3621

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 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
2		an12 645	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
3	2	exbii 1848	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 278	. 2 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5		eleq1 2816	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		ceqsrexv.1	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	7	ceqsexgv 3620	. . 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 3053

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  ceqsrexbv  3622  ceqsrex2v  3624  reuxfrd  3719  f1oiso  7326  creur  12180  creui  12181  deg1ldg  25997  ulm2  26294  iscgra1  28737  reuxfrdf  32420  poimirlem24  37638  eqlkr3  39094  diclspsn  41188  rmxdiophlem  43004  expdiophlem1  43010  expdiophlem2  43011