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

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

Proof of Theorem ralab
StepHypRef Expression
1 df-ral 3141 . 2 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒))
2 vex 3496 . . . . 5 𝑥 ∈ V
3 ralab.1 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
42, 3elab 3665 . . . 4 (𝑥 ∈ {𝑦𝜑} ↔ 𝜓)
54imbi1i 352 . . 3 ((𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ (𝜓𝜒))
65albii 1813 . 2 (∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ ∀𝑥(𝜓𝜒))
71, 6bitri 277 1 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1528   ∈ wcel 2107  {cab 2797  ∀wral 3136 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-v 3495 This theorem is referenced by:  ralrnmpo  7281  funcnvuni  7628  kardex  9315  karden  9316  fimaxre3  11579  ptcnp  22222  ptrescn  22239  itg2leub  24327  nmoubi  28541  nmopub  29677  nmfnleub  29694  nmcexi  29795  mblfinlem3  34923  ismblfin  34925  itg2addnc  34938  hbtlem2  39714
 Copyright terms: Public domain W3C validator