Theorem brtxpsd2

Description: Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-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$$
Assertion	brtxpsd2	$$⊢ARB\leftrightarrow \forall x\left(x\in B\leftrightarrow xSA\right)$$

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	3	breqi	$$⊢ARB\leftrightarrow A\left(C\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)\right)B$$
6		brdif	$$⊢A\left(C\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)\right)B\leftrightarrow \left(ACB\wedge \neg A\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)B\right)$$
7	5 6	bitri	$$⊢ARB\leftrightarrow \left(ACB\wedge \neg A\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)B\right)$$
8	4 7	mpbiran	$$⊢ARB\leftrightarrow \neg A\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)B$$
9	1 2	brtxpsd	$$⊢\neg A\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(S\otimes \mathrm{V}\right)\right)B\leftrightarrow \forall x\left(x\in B\leftrightarrow xSA\right)$$
10	8 9	bitri	$$⊢ARB\leftrightarrow \forall x\left(x\in B\leftrightarrow xSA\right)$$