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

Theorem ralrab 3687
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 3681 . . . 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  5652  wereu2  5669  frpomin  6333  weniso  7338  zmin  12915  prmreclem1  16836  lublecllem  18300  mhmeql  18694  ghmeql  19100  pgpfac1lem5  19932  lmhmeql  20643  islindf4  21366  1stcfb  22918  fbssfi  23310  filssufilg  23384  txflf  23479  ptcmplem3  23527  symgtgp  23579  tgpconncompeqg  23585  cnllycmp  24441  ovolgelb  24966  dyadmax  25084  lhop1  25500  radcnvlt1  25899  noextenddif  27138  conway  27267  madebdaylemlrcut  27360  poimirlem4  36397  poimirlem32  36425  ismblfin  36434  igenval2  36840  glbconN  38153  glbconNOLD  38154  nadd2rabtr  42005  mgmhmeql  46446  intubeu  47449  unilbeu  47450
  Copyright terms: Public domain W3C validator