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

Theorem ralrab 3690
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 3684 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32imbi1i 350 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ ((𝑥𝐴𝜓) → 𝜒))
4 impexp 452 . . 3 (((𝑥𝐴𝜓) → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
53, 4bitri 275 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
65ralbii2 3090 1 (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wral 3062  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477
This theorem is referenced by:  frminex  5657  wereu2  5674  frpomin  6342  weniso  7351  zmin  12928  prmreclem1  16849  lublecllem  18313  mhmeql  18707  ghmeql  19115  pgpfac1lem5  19949  lmhmeql  20666  islindf4  21393  1stcfb  22949  fbssfi  23341  filssufilg  23415  txflf  23510  ptcmplem3  23558  symgtgp  23610  tgpconncompeqg  23616  cnllycmp  24472  ovolgelb  24997  dyadmax  25115  lhop1  25531  radcnvlt1  25930  noextenddif  27171  conway  27300  madebdaylemlrcut  27393  poimirlem4  36492  poimirlem32  36520  ismblfin  36529  igenval2  36934  glbconN  38247  glbconNOLD  38248  nadd2rabtr  42134  mgmhmeql  46573  intubeu  47609  unilbeu  47610
  Copyright terms: Public domain W3C validator