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 ) )