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

Theorem ralrab 3507
 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 3502 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32imbi1i 338 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ ((𝑥𝐴𝜓) → 𝜒))
4 impexp 461 . . 3 (((𝑥𝐴𝜓) → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
53, 4bitri 264 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
65ralbii2 3114 1 (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2137  ∀wral 3048  {crab 3052 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rab 3057  df-v 3340 This theorem is referenced by:  frminex  5244  wereu2  5261  weniso  6765  zmin  11975  prmreclem1  15820  lublecllem  17187  mhmeql  17563  ghmeql  17882  pgpfac1lem5  18676  lmhmeql  19255  islindf4  20377  1stcfb  21448  fbssfi  21840  filssufilg  21914  txflf  22009  ptcmplem3  22057  symgtgp  22104  tgpconncompeqg  22114  cnllycmp  22954  ovolgelb  23446  dyadmax  23564  lhop1  23974  radcnvlt1  24369  frpomin  32042  noextenddif  32125  conway  32214  poimirlem4  33724  poimirlem32  33752  ismblfin  33761  igenval2  34176  glbconN  35164  mgmhmeql  42311
 Copyright terms: Public domain W3C validator