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

Theorem ralrab 3335
Description: Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypothesis
Ref Expression
ralab.1 (𝑦 = 𝑥 → (𝜑𝜓))
Assertion
Ref Expression
ralrab (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralrab
StepHypRef Expression
1 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
21elrab 3331 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32imbi1i 338 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ ((𝑥𝐴𝜓) → 𝜒))
4 impexp 461 . . 3 (((𝑥𝐴𝜓) → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
53, 4bitri 263 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
65ralbii2 2961 1 (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  wcel 1977  wral 2896  {crab 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175
This theorem is referenced by:  frminex  5018  wereu2  5035  weniso  6504  zmin  11660  prmreclem1  15458  lublecllem  16811  mhmeql  17187  ghmeql  17506  pgpfac1lem5  18301  lmhmeql  18876  islindf4  19996  1stcfb  21058  fbssfi  21451  filssufilg  21525  txflf  21620  ptcmplem3  21668  symgtgp  21715  tgpconcompeqg  21725  cnllycmp  22563  ovolgelb  23055  dyadmax  23172  lhop1  23581  radcnvlt1  23976  uvtxnb  26025  2spotdisj  26588  poimirlem4  32583  poimirlem32  32611  ismblfin  32620  igenval2  33035  glbconN  33681  mgmhmeql  41593
  Copyright terms: Public domain W3C validator