Theorem bj-rexcom4b

Description: Remove from rexcom4b dependency on ax-ext and ax-13 (and on df-or , df-cleq , df-nfc , df-v ). The hypothesis uses V instead of _V (see bj-isseti for the motivation). Use bj-rexcom4bv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-rexcom4b.1	|- B e. V
Assertion	bj-rexcom4b	|- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ph )

Proof

Step	Hyp	Ref	Expression
1		bj-rexcom4b.1	|- B e. V
2		rexcom4a	|- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ( ph /\ E. x x = B ) )
3	1	bj-isseti	|- E. x x = B
4	3	biantru	|- ( ph <-> ( ph /\ E. x x = B ) )
5	4	rexbii	|- ( E. y e. A ph <-> E. y e. A ( ph /\ E. x x = B ) )
6	2 5	bitr4i	|- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ph )