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

Theorem ralab 3697
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 3062 . 2 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒))
2 df-clab 2715 . . . . . 6 (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
3 ralab.1 . . . . . . 7 (𝑦 = 𝑥 → (𝜑𝜓))
43sbievw 2093 . . . . . 6 ([𝑥 / 𝑦]𝜑𝜓)
52, 4bitri 275 . . . . 5 (𝑥 ∈ {𝑦𝜑} ↔ 𝜓)
65imbi1i 349 . . . 4 ((𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ (𝜓𝜒))
7 biid 261 . . . 4 ((𝜓𝜒) ↔ (𝜓𝜒))
86, 7bitri 275 . . 3 ((𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ (𝜓𝜒))
98albii 1819 . 2 (∀𝑥(𝑥 ∈ {𝑦𝜑} → 𝜒) ↔ ∀𝑥(𝜓𝜒))
101, 9bitri 275 1 (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  [wsb 2064  wcel 2108  {cab 2714  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-ral 3062
This theorem is referenced by:  rexab  3700  ralrnmpo  7572  funcnvuni  7954  kardex  9934  karden  9935  fimaxre3  12214  ptcnp  23630  ptrescn  23647  itg2leub  25769  addsuniflem  28034  addsbdaylem  28049  mulsuniflem  28175  nmoubi  30791  nmopub  31927  nmfnleub  31944  nmcexi  32045  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  hbtlem2  43136  oaun3lem1  43387
  Copyright terms: Public domain W3C validator