Theorem ralab 3634

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 3054	. 2 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒))
2		df-clab 2718	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
3		ralab.1	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
4	3	sbievw 2104	. . . . 5 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜓)
5	2, 4	bitri 276	. . . 4 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ 𝜓)
6	5	imbi1i 350	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ (𝜓 → 𝜒))
7	6	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝑦 ∣ 𝜑} → 𝜒) ↔ ∀𝑥(𝜓 → 𝜒))
8	1, 7	bitri 276	1 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  [wsb 2073   ∈ wcel 2119  {cab 2717  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-ral 3054

This theorem is referenced by:  rexab  3636  ralrnmpo  7495  funcnvuni  7872  kardex  9809  karden  9810  fimaxre3  12093  ptcnp  23605  ptrescn  23622  itg2leub  25719  addsuniflem  28011  addbdaylem  28027  mulsuniflem  28159  nmoubi  30861  nmopub  31997  nmfnleub  32014  nmcexi  32115  mblfinlem3  38026  ismblfin  38028  itg2addnc  38041  hbtlem2  43569  oaun3lem1  43819