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

Step	Hyp	Ref	Expression
1		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒))
2		df-clab 2715	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
3		ralab.1	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
4	3	sbievw 2093	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜓)
5	2, 4	bitri 275	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ 𝜓)
6	5	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒))
7		biid 261	. . . 4 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜒))
8	6, 7	bitri 275	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒))
9	8	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒))
10	1, 9	bitri 275	1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒))

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