This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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{˙}{[} y / x \underset{˙}{]} (x \in a \land a \cap x = \emptyset) \leftrightarrow (y \in a \land a \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		sbcan	$⊢ \underset{˙}{[} y / x \underset{˙}{]} (x \in a \land a \cap x = \emptyset) \leftrightarrow (\underset{˙}{[} y / x \underset{˙}{]} x \in a \land \underset{˙}{[} y / x \underset{˙}{]} a \cap x = \emptyset)$
2		sbcel1v	$⊢ \underset{˙}{[} y / x \underset{˙}{]} x \in a \leftrightarrow y \in a$
3		vex	$⊢ y \in V$
4		sbceqg	$⊢ y \in V \to (\underset{˙}{[} y / x \underset{˙}{]} a \cap x = \emptyset \leftrightarrow ⦋ y / x ⦌ (a \cap x) = ⦋ y / x ⦌ \emptyset)$
5	3 4	ax-mp	$⊢ \underset{˙}{[} y / x \underset{˙}{]} a \cap x = \emptyset \leftrightarrow ⦋ y / x ⦌ (a \cap x) = ⦋ y / x ⦌ \emptyset$
6		csbin	$⊢ ⦋ y / x ⦌ (a \cap x) = ⦋ y / x ⦌ a \cap ⦋ y / x ⦌ x$
7		csbconstg	$⊢ y \in V \to ⦋ y / x ⦌ a = a$
8	3 7	ax-mp	$⊢ ⦋ y / x ⦌ a = a$
9		csbvarg	$⊢ y \in 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 ⦌ (a \cap x) = a \cap y$
13		csb0	$⊢ ⦋ y / x ⦌ \emptyset = \emptyset$
14	12 13	eqeq12i	$⊢ ⦋ y / x ⦌ (a \cap x) = ⦋ y / x ⦌ \emptyset \leftrightarrow a \cap y = \emptyset$
15	5 14	bitri	$⊢ \underset{˙}{[} y / x \underset{˙}{]} a \cap x = \emptyset \leftrightarrow a \cap y = \emptyset$
16	2 15	anbi12i	$⊢ (\underset{˙}{[} y / x \underset{˙}{]} x \in a \land \underset{˙}{[} y / x \underset{˙}{]} a \cap x = \emptyset) \leftrightarrow (y \in a \land a \cap y = \emptyset)$
17	1 16	bitri	$⊢ \underset{˙}{[} y / x \underset{˙}{]} (x \in a \land a \cap x = \emptyset) \leftrightarrow (y \in a \land a \cap y = \emptyset)$