Theorem rexcom4b

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

	Ref	Expression
Hypothesis	rexcom4b.1	$$⊢B\in \mathrm{V}$$
Assertion	rexcom4b	$$⊢\exists x\exists y\in A\left(\phi \wedge x=B\right)\leftrightarrow \exists y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexcom4b.1	$$⊢B\in \mathrm{V}$$
2		rexcom4a	$$⊢\exists x\exists y\in A\left(\phi \wedge x=B\right)\leftrightarrow \exists y\in A\left(\phi \wedge \exists xx=B\right)$$
3	1	isseti	$$⊢\exists xx=B$$
4	3	biantru	$$⊢\phi \leftrightarrow \left(\phi \wedge \exists xx=B\right)$$
5	4	rexbii	$$⊢\exists y\in A\phi \leftrightarrow \exists y\in A\left(\phi \wedge \exists xx=B\right)$$
6	2 5	bitr4i	$$⊢\exists x\exists y\in A\left(\phi \wedge x=B\right)\leftrightarrow \exists y\in A\phi$$