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

Theorem ralrab 3401
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 3396 . . . 4 (𝑥 ∈ {𝑦𝐴𝜑} ↔ (𝑥𝐴𝜓))
32imbi1i 338 . . 3 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ ((𝑥𝐴𝜓) → 𝜒))
4 impexp 461 . . 3 (((𝑥𝐴𝜓) → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
53, 4bitri 264 . 2 ((𝑥 ∈ {𝑦𝐴𝜑} → 𝜒) ↔ (𝑥𝐴 → (𝜓𝜒)))
65ralbii2 3007 1 (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  wral 2941  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233
This theorem is referenced by:  frminex  5123  wereu2  5140  weniso  6644  zmin  11822  prmreclem1  15667  lublecllem  17035  mhmeql  17411  ghmeql  17730  pgpfac1lem5  18524  lmhmeql  19103  islindf4  20225  1stcfb  21296  fbssfi  21688  filssufilg  21762  txflf  21857  ptcmplem3  21905  symgtgp  21952  tgpconncompeqg  21962  cnllycmp  22802  ovolgelb  23294  dyadmax  23412  lhop1  23822  radcnvlt1  24217  frpomin  31863  noextenddif  31946  conway  32035  poimirlem4  33543  poimirlem32  33571  ismblfin  33580  igenval2  33995  glbconN  34981  mgmhmeql  42128
  Copyright terms: Public domain W3C validator