This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralab

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

Ref Expression
Hypothesis ralab.1 
|- ( y = x -> ( ph <-> ps ) )
Assertion ralab 
|- ( A. x e. { y | ph } ch <-> A. x ( ps -> ch ) )

Proof

Step Hyp Ref Expression
1 ralab.1 
 |-  ( y = x -> ( ph <-> ps ) )
2 df-ral 
 |-  ( A. x e. { y | ph } ch <-> A. x ( x e. { y | ph } -> ch ) )
3 df-clab 
 |-  ( x e. { y | ph } <-> [ x / y ] ph )
4 1 sbievw 
 |-  ( [ x / y ] ph <-> ps )
5 3 4 bitri 
 |-  ( x e. { y | ph } <-> ps )
6 5 imbi1i 
 |-  ( ( x e. { y | ph } -> ch ) <-> ( ps -> ch ) )
7 biid 
 |-  ( ( ps -> ch ) <-> ( ps -> ch ) )
8 6 7 bitri 
 |-  ( ( x e. { y | ph } -> ch ) <-> ( ps -> ch ) )
9 8 albii 
 |-  ( A. x ( x e. { y | ph } -> ch ) <-> A. x ( ps -> ch ) )
10 2 9 bitri 
 |-  ( A. x e. { y | ph } ch <-> A. x ( ps -> ch ) )