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

Theorem rexrab 3691
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 3684 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32anbi1i 623 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} ∧ 𝜒) ↔ ((𝑥𝐴𝜓) ∧ 𝜒))
4 anass 469 . . 3 (((𝑥𝐴𝜓) ∧ 𝜒) ↔ (𝑥𝐴 ∧ (𝜓𝜒)))
53, 4bitri 276 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} ∧ 𝜒) ↔ (𝑥𝐴 ∧ (𝜓𝜒)))
65rexbii2 3250 1 (∃𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∃𝑥𝐴 (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2107  wrex 3144  {crab 3147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502
This theorem is referenced by:  wereu2  5551  wdom2d  9038  enfin2i  9737  infm3  11594  pmtrfrn  18522  pgpssslw  18675  ellspd  20881  1stcfb  21988  xkobval  22129  xkococn  22203  imasdsf1olem  22917  rusgrnumwwlks  27686  cvmliftlem15  32448  frpomin  32981  wsuclem  33015  scutun12  33174  poimirlem4  34782  poimirlem26  34804  poimirlem27  34805  rexrabdioph  39275  hbtlem6  39613
  Copyright terms: Public domain W3C validator