Theorem ralab 3664

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 3045	. 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒))
2		df-clab 2708	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
3		ralab.1	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
4	3	sbievw 2094	. . . . . 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 2065   ∈ wcel 2109  {cab 2707  ∀wral 3044

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 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-ral 3045

This theorem is referenced by:  rexab  3666  ralrnmpo  7528  funcnvuni  7908  kardex  9847  karden  9848  fimaxre3  12129  ptcnp  23509  ptrescn  23526  itg2leub  25635  addsuniflem  27908  addsbdaylem  27923  mulsuniflem  28052  nmoubi  30701  nmopub  31837  nmfnleub  31854  nmcexi  31955  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  hbtlem2  43113  oaun3lem1  43363