Theorem ralab 3653

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 3053	. 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒))
2		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
3		ralab.1	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
4	3	sbievw 2099	. . . . . 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 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒))
10	1, 9	bitri 275	1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  [wsb 2068   ∈ wcel 2114  {cab 2715  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-ral 3053

This theorem is referenced by:  rexab  3655  ralrnmpo  7507  funcnvuni  7884  kardex  9818  karden  9819  fimaxre3  12100  ptcnp  23578  ptrescn  23595  itg2leub  25703  addsuniflem  28009  addbdaylem  28025  mulsuniflem  28157  nmoubi  30859  nmopub  31995  nmfnleub  32012  nmcexi  32113  mblfinlem3  37907  ismblfin  37909  itg2addnc  37922  hbtlem2  43478  oaun3lem1  43728