Theorem onfrALTlem4

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onfrALTlem4	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(x\in a\wedge a\cap x=\varnothing \right)\leftrightarrow \left(y\in a\wedge a\cap y=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcan	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(x\in a\wedge a\cap x=\varnothing \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x\in a\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}a\cap x=\varnothing \right)$$
2		sbcel1v	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x\in a\leftrightarrow y\in a$$
3		vex	$$⊢y\in \mathrm{V}$$
4		sbceqg	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}a\cap x=\varnothing \leftrightarrow ⦋y/x⦌\left(a\cap x\right)=⦋y/x⦌\varnothing \right)$$
5	3 4	ax-mp	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}a\cap x=\varnothing \leftrightarrow ⦋y/x⦌\left(a\cap x\right)=⦋y/x⦌\varnothing$$
6		csbin	$$⊢⦋y/x⦌\left(a\cap x\right)=⦋y/x⦌a\cap ⦋y/x⦌x$$
7		csbconstg	$$⊢y\in \mathrm{V}\to ⦋y/x⦌a=a$$
8	3 7	ax-mp	$$⊢⦋y/x⦌a=a$$
9		csbvarg	$$⊢y\in \mathrm{V}\to ⦋y/x⦌x=y$$
10	3 9	ax-mp	$$⊢⦋y/x⦌x=y$$
11	8 10	ineq12i	$$⊢⦋y/x⦌a\cap ⦋y/x⦌x=a\cap y$$
12	6 11	eqtri	$$⊢⦋y/x⦌\left(a\cap x\right)=a\cap y$$
13		csb0	$$⊢⦋y/x⦌\varnothing =\varnothing$$
14	12 13	eqeq12i	$$⊢⦋y/x⦌\left(a\cap x\right)=⦋y/x⦌\varnothing \leftrightarrow a\cap y=\varnothing$$
15	5 14	bitri	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}a\cap x=\varnothing \leftrightarrow a\cap y=\varnothing$$
16	2 15	anbi12i	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x\in a\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}a\cap x=\varnothing \right)\leftrightarrow \left(y\in a\wedge a\cap y=\varnothing \right)$$
17	1 16	bitri	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(x\in a\wedge a\cap x=\varnothing \right)\leftrightarrow \left(y\in a\wedge a\cap y=\varnothing \right)$$