Theorem ralab 3628

Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) Reduce axiom usage. (Revised by Gino Giotto, 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 3069	. 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒))
2		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
3		ralab.1	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
4	3	sbievw 2095	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜓)
5	2, 4	bitri 274	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ 𝜓)
6	5	imbi1i 350	. . . 4 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒))
7		biid 260	. . . 4 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜒))
8	6, 7	bitri 274	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒))
9	8	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒))
10	1, 9	bitri 274	1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  [wsb 2067   ∈ wcel 2106  {cab 2715  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-ral 3069

This theorem is referenced by:  rexab  3631  ralrnmpo  7412  funcnvuni  7778  kardex  9652  karden  9653  fimaxre3  11921  ptcnp  22773  ptrescn  22790  itg2leub  24899  nmoubi  29134  nmopub  30270  nmfnleub  30287  nmcexi  30388  mblfinlem3  35816  ismblfin  35818  itg2addnc  35831  hbtlem2  40949