Metamath Proof Explorer

Theorem ralab

Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024)

Ref Expression
Hypothesis ralab.1 ⊢ y = x → φ ↔ ψ
Assertion ralab ⊢ ∀ x ∈ y | φ χ ↔ ∀ x ψ → χ

Proof

Step Hyp Ref Expression
1 ralab.1 ⊢ y = x → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ y | φ χ ↔ ∀ x x ∈ y | φ → χ
3 df-clab ⊢ x ∈ y | φ ↔ x y φ
4 1 sbievw ⊢ x y φ ↔ ψ
5 3 4 bitri ⊢ x ∈ y | φ ↔ ψ
6 5 imbi1i ⊢ x ∈ y | φ → χ ↔ ψ → χ
7 biid ⊢ ψ → χ ↔ ψ → χ
8 6 7 bitri ⊢ x ∈ y | φ → χ ↔ ψ → χ
9 8 albii ⊢ ∀ x x ∈ y | φ → χ ↔ ∀ x ψ → χ
10 2 9 bitri ⊢ ∀ x ∈ y | φ χ ↔ ∀ x ψ → χ