Theorem rexcom4b

Description: Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		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	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 )