Theorem sbcoreleleqVD

Description: Virtual deduction proof of sbcoreleleq . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

	Ref	Expression
Assertion	sbcoreleleqVD	$$⊢A\in B\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		sbcor	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(\left(x\in y\vee y\in x\right)\vee x=y\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)$$
2	1	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(\left(x\in y\vee y\in x\right)\vee x=y\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\right)$$
3		df-3or	$$⊢\left(x\in y\vee y\in x\vee x=y\right)\leftrightarrow \left(\left(x\in y\vee y\in x\right)\vee x=y\right)$$
4	3	bicomi	$$⊢\left(\left(x\in y\vee y\in x\right)\vee x=y\right)\leftrightarrow \left(x\in y\vee y\in x\vee x=y\right)$$
5	4	sbcbii	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(\left(x\in y\vee y\in x\right)\vee x=y\right)\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)$$
6	5	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(\left(x\in y\vee y\in x\right)\vee x=y\right)\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)\right)$$
7		sbcor	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\right)$$
8	7	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\right)\right)$$
9	8	orbi1d	$$⊢A\in B\to \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\right)$$
10	2 6 9	3bitr3d	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\left(x\in y\vee y\in x\vee x=y\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)\right)$$
11		df-3or	$$⊢\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(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\right)\vee \underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\right)$$
12	10 11	bitr4di	$$⊢A\in B\to \left(\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)\right)$$
13	12	dfvd1ir	$$⊢\left(A\in B\to \left(\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)\right)\right)$$
14		sbcel2gv	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\leftrightarrow x\in A\right)$$
15	14	dfvd1ir	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x\in y\leftrightarrow x\in A\right)\right)$$
16		sbcel1v	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y\in x\leftrightarrow A\in x$$
17		eqsbc2	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\leftrightarrow x=A\right)$$
18	17	dfvd1ir	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}x=y\leftrightarrow x=A\right)\right)$$
19		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)$$
20	19	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)$$
21	15 16 18 20	e101	$$⊢\left(A\in B\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)$$
22		biantr	$$⊢\left(\left(\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)\right)\wedge \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)\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)$$
23	13 21 22	e11an	$$⊢\left(A\in B\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)\right)$$
24	23	in1	$$⊢A\in B\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)$$