Theorem rexrab 3718

Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)

Hypothesis

Ref	Expression
ralab.1	⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rexrab	⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))

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

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexrab

Step	Hyp	Ref	Expression
1		ralab.1	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
2	1	elrab 3708	. . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	anbi1i 623	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒))
4		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒)))
5	3, 4	bitri 275	. 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∧ 𝜒) ↔ (𝑥 ∈ 𝐴 ∧ (𝜓 ∧ 𝜒)))
6	5	rexbii2 3096	1 ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490

This theorem is referenced by:  wereu2  5697  frpomin  6372  wdom2d  9649  enfin2i  10390  infm3  12254  pmtrfrn  19500  pgpssslw  19656  ellspd  21845  1stcfb  23474  xkobval  23615  xkococn  23689  imasdsf1olem  24404  eqscut2  27869  scutun12  27873  cuteq0  27895  rusgrnumwwlks  30007  cvmliftlem15  35266  wsuclem  35789  poimirlem4  37584  poimirlem26  37606  poimirlem27  37607  infdesc  42598  rexrabdioph  42750  hbtlem6  43086  uhgrimisgrgric  47783  uspgrlimlem1  47812