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

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

Proof of Theorem ralab
StepHypRef Expression
1 df-ral 3060 . 2 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒))
2 df-clab 2713 . . . . . 6 (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
3 ralab.1 . . . . . . 7 (𝑦 = 𝑥 → (𝜑𝜓))
43sbievw 2091 . . . . . 6 ([𝑥 / 𝑦]𝜑𝜓)
52, 4bitri 275 . . . . 5 (𝑥 ∈ {𝑦𝜑} ↔ 𝜓)
65imbi1i 349 . . . 4 ((𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ (𝜓𝜒))
7 biid 261 . . . 4 ((𝜓𝜒) ↔ (𝜓𝜒))
86, 7bitri 275 . . 3 ((𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ (𝜓𝜒))
98albii 1816 . 2 (∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ ∀𝑥(𝜓𝜒))
101, 9bitri 275 1 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  [wsb 2062  wcel 2106  {cab 2712  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-ral 3060
This theorem is referenced by:  rexab  3703  ralrnmpo  7572  funcnvuni  7955  kardex  9932  karden  9933  fimaxre3  12212  ptcnp  23646  ptrescn  23663  itg2leub  25784  addsuniflem  28049  addsbdaylem  28064  mulsuniflem  28190  nmoubi  30801  nmopub  31937  nmfnleub  31954  nmcexi  32055  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  hbtlem2  43113  oaun3lem1  43364
  Copyright terms: Public domain W3C validator