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 -> ( ps <-> ch ) )
Assertion ralab2
|- ( A. x e. { y | ph } ps <-> A. y ( ph -> ch ) )

Proof

Step Hyp Ref Expression
1 ralab2.1
 |-  ( x = y -> ( ps <-> ch ) )
2 df-ral
 |-  ( A. x e. { y | ph } ps <-> A. x ( x e. { y | ph } -> ps ) )
3 nfsab1
 |-  F/ y x e. { y | ph }
4 nfv
 |-  F/ y ps
5 3 4 nfim
 |-  F/ y ( x e. { y | ph } -> ps )
6 nfv
 |-  F/ x ( ph -> ch )
7 eleq1ab
 |-  ( x = y -> ( x e. { y | ph } <-> y e. { y | ph } ) )
8 abid
 |-  ( y e. { y | ph } <-> ph )
9 7 8 bitrdi
 |-  ( x = y -> ( x e. { y | ph } <-> ph ) )
10 9 1 imbi12d
 |-  ( x = y -> ( ( x e. { y | ph } -> ps ) <-> ( ph -> ch ) ) )
11 5 6 10 cbvalv1
 |-  ( A. x ( x e. { y | ph } -> ps ) <-> A. y ( ph -> ch ) )
12 2 11 bitri
 |-  ( A. x e. { y | ph } ps <-> A. y ( ph -> ch ) )