Metamath Proof Explorer


Theorem ralab2

Description: Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

Ref Expression
Hypothesis ralab2.1 x = y ψ χ
Assertion ralab2 x y | φ ψ y φ χ

Proof

Step Hyp Ref Expression
1 ralab2.1 x = y ψ χ
2 df-ral x y | φ ψ x x y | φ ψ
3 nfsab1 y x y | φ
4 nfv y ψ
5 3 4 nfim y x y | φ ψ
6 nfv x φ χ
7 eleq1ab x = y x y | φ y y | φ
8 abid y y | φ φ
9 7 8 bitrdi x = y x y | φ φ
10 9 1 imbi12d x = y x y | φ ψ φ χ
11 5 6 10 cbvalv1 x x y | φ ψ y φ χ
12 2 11 bitri x y | φ ψ y φ χ