MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexrab Structured version   Visualization version   GIF version

Theorem rexrab 3702
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
StepHypRef Expression
1 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
21elrab 3692 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32anbi1i 624 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} ∧ 𝜒) ↔ ((𝑥𝐴𝜓) ∧ 𝜒))
4 anass 468 . . 3 (((𝑥𝐴𝜓) ∧ 𝜒) ↔ (𝑥𝐴 ∧ (𝜓𝜒)))
53, 4bitri 275 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} ∧ 𝜒) ↔ (𝑥𝐴 ∧ (𝜓𝜒)))
65rexbii2 3090 1 (∃𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∃𝑥𝐴 (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2108  wrex 3070  {crab 3436
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482
This theorem is referenced by:  wereu2  5682  frpomin  6361  wdom2d  9620  enfin2i  10361  infm3  12227  pmtrfrn  19476  pgpssslw  19632  ellspd  21822  1stcfb  23453  xkobval  23594  xkococn  23668  imasdsf1olem  24383  eqscut2  27851  scutun12  27855  cuteq0  27877  rusgrnumwwlks  29994  cvmliftlem15  35303  wsuclem  35826  poimirlem4  37631  poimirlem26  37653  poimirlem27  37654  infdesc  42653  rexrabdioph  42805  hbtlem6  43141  uhgrimisgrgric  47899  uspgrlimlem1  47955
  Copyright terms: Public domain W3C validator