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

Metamath Proof Explorer

Theorem rexab

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014) (Revised by Mario Carneiro, 3-Sep-2015) Reduce axiom usage. (Revised by GG, 2-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 ralab.1 
 |-  ( y = x -> ( ph <-> ps ) )
2 dfrex2 
 |-  ( E. x e. { y | ph } ch <-> -. A. x e. { y | ph } -. ch )
3 1 ralab 
 |-  ( A. x e. { y | ph } -. ch <-> A. x ( ps -> -. ch ) )
4 2 3 xchbinx 
 |-  ( E. x e. { y | ph } ch <-> -. A. x ( ps -> -. ch ) )
5 imnang 
 |-  ( A. x ( ps -> -. ch ) <-> A. x -. ( ps /\ ch ) )
6 4 5 xchbinx 
 |-  ( E. x e. { y | ph } ch <-> -. A. x -. ( ps /\ ch ) )
7 df-ex 
 |-  ( E. x ( ps /\ ch ) <-> -. A. x -. ( ps /\ ch ) )
8 6 7 bitr4i 
 |-  ( E. x e. { y | ph } ch <-> E. x ( ps /\ ch ) )