Theorem brtxpsd3

Description: A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Hypotheses	brtxpsd2.1	$$⊢A\in \mathrm{V}$$
	brtxpsd2.2	$$⊢B\in \mathrm{V}$$
	brtxpsd2.3	$$⊢R=C\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)$$
	brtxpsd2.4	$$⊢ACB$$
	brtxpsd3.5	$$⊢x\in X\leftrightarrow xSA$$
Assertion	brtxpsd3	$$⊢ARB\leftrightarrow B=X$$

Proof

Step	Hyp	Ref	Expression
1		brtxpsd2.1	$$⊢A\in \mathrm{V}$$
2		brtxpsd2.2	$$⊢B\in \mathrm{V}$$
3		brtxpsd2.3	$$⊢R=C\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)$$
4		brtxpsd2.4	$$⊢ACB$$
5		brtxpsd3.5	$$⊢x\in X\leftrightarrow xSA$$
6	5	bibi2i	$$⊢\left(x\in B\leftrightarrow x\in X\right)\leftrightarrow \left(x\in B\leftrightarrow xSA\right)$$
7	6	albii	$$⊢\forall x\left(x\in B\leftrightarrow x\in X\right)\leftrightarrow \forall x\left(x\in B\leftrightarrow xSA\right)$$
8		dfcleq	$$⊢B=X\leftrightarrow \forall x\left(x\in B\leftrightarrow x\in X\right)$$
9	1 2 3 4	brtxpsd2	$$⊢ARB\leftrightarrow \forall x\left(x\in B\leftrightarrow xSA\right)$$
10	7 8 9	3bitr4ri	$$⊢ARB\leftrightarrow B=X$$