Theorem ceqsrexv 3593

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 3064	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
2		an12 651	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
3	2	exbii 1855	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 279	. 2 ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5		eleq1 2827	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		ceqsrexv.1	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 638	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	7	ceqsexgv 3592	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	8	bianabs 546	. 2 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ 𝜓))
10	4, 9	bitrid 284	1 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064

This theorem is referenced by:  ceqsrexbv  3594  ceqsrex2v  3596  reuxfrd  3689  f1oiso  7295  creur  12144  creui  12145  deg1ldg  26075  ulm2  26368  iscgra1  28896  reuxfrdf  32578  poimirlem24  38011  eqlkr3  39593  diclspsn  41686  rmxdiophlem  43460  expdiophlem1  43466  expdiophlem2  43467