Theorem bj-rexvw

Description: A weak version of rexv not using ax-ext (nor df-cleq , df-clel , df-v ), and only core FOL axioms. See also bj-ralvw . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-rexvw.1	|- ps
Assertion	bj-rexvw	|- ( E. x e. { y | ps } ph <-> E. x ph )

Proof

Step	Hyp	Ref	Expression
1		bj-rexvw.1	|- ps
2		df-rex	|- ( E. x e. { y | ps } ph <-> E. x ( x e. { y | ps } /\ ph ) )
3	1	vexw	|- x e. { y | ps }
4	3	biantrur	|- ( ph <-> ( x e. { y | ps } /\ ph ) )
5	4	exbii	|- ( E. x ph <-> E. x ( x e. { y | ps } /\ ph ) )
6	2 5	bitr4i	|- ( E. x e. { y | ps } ph <-> E. x ph )