Theorem sbcoreleleq

Description: Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbcoreleleq	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)\leftrightarrow \left(x\in A\vee A\in x\vee x=A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbc3or	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)$$
2		sbcel2gv	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\leftrightarrow x\in A\right)$$
3		sbcel1v	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\leftrightarrow A\in x$$
4	3	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\leftrightarrow A\in x\right)$$
5		eqsbc2	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\leftrightarrow x=A\right)$$
6		3orbi123	$$⊢\left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\leftrightarrow x\in A\right)\wedge \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\leftrightarrow A\in x\right)\wedge \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\leftrightarrow x=A\right)\right)\to \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\leftrightarrow \left(x\in A\vee A\in x\vee x=A\right)\right)$$
7	6	3impexpbicomi	$$⊢\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\leftrightarrow x\in A\right)\to \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\leftrightarrow A\in x\right)\to \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\leftrightarrow x=A\right)\to \left(\left(x\in A\vee A\in x\vee x=A\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\right)\right)\right)$$
8	2 4 5 7	syl3c	$$⊢A\in V\to \left(\left(x\in A\vee A\in x\vee x=A\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\right)$$
9	1 8	bitr4id	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)\leftrightarrow \left(x\in A\vee A\in x\vee x=A\right)\right)$$