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\in V$$
Assertion	bj-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		bj-rexcom4b.1	$$⊢B\in 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	bj-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$$