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

Metamath Proof Explorer

Theorem rexab2

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

Ref Expression
Hypothesis ralab2.1 
|- ( x = y -> ( ps <-> ch ) )
Assertion rexab2 
|- ( E. x e. { y | ph } ps <-> E. y ( ph /\ ch ) )

Proof

Step Hyp Ref Expression
1 ralab2.1 
 |-  ( x = y -> ( ps <-> ch ) )
2 df-rex 
 |-  ( E. x e. { y | ph } ps <-> E. x ( x e. { y | ph } /\ ps ) )
3 nfsab1 
 |-  F/ y x e. { y | ph }
4 nfv 
 |-  F/ y ps
5 3 4 nfan 
 |-  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 anbi12d 
 |-  ( x = y -> ( ( x e. { y | ph } /\ ps ) <-> ( ph /\ ch ) ) )
11 5 6 10 cbvexv1 
 |-  ( E. x ( x e. { y | ph } /\ ps ) <-> E. y ( ph /\ ch ) )
12 2 11 bitri 
 |-  ( E. x e. { y | ph } ps <-> E. y ( ph /\ ch ) )