Theorem sbcssgVD

Description: Virtual deduction proof of sbcssg . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcssg is sbcssgVD without virtual deductions and was automatically derived from sbcssgVD .

	Ref	Expression
Assertion	sbcssgVD	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow ⦋A/x⦌C\subseteq ⦋A/x⦌D\right)$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in B\to A\in B\right)$$
2		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C$$
3	2	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)$$
4	1 3	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
5		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D$$
6	5	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)$$
7	1 6	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)\right)$$
8		imbi12	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
9	4 7 8	e11	$$⊢\left(A\in B\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
10		sbcimg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)$$
11	1 10	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\right)$$
12		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
13	12	biimprcd	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
14	9 11 13	e11	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
15	14	gen11	$$⊢\left(A\in B\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
16		albi	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)$$
17	15 16	e1a	$$⊢\left(A\in B\to \left(\forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
18		sbcal	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)$$
19	18	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\right)$$
20	1 19	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\right)\right)$$
21		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\leftrightarrow \left(\forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
22	21	biimprcd	$$⊢\left(\forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\to y\in D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
23	17 20 22	e11	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
24		df-ss	$$⊢C\subseteq D\leftrightarrow \forall y\left(y\in C\to y\in D\right)$$
25	24	ax-gen	$$⊢\forall x\left(C\subseteq D\leftrightarrow \forall y\left(y\in C\to y\in D\right)\right)$$
26		sbcbi	$$⊢A\in B\to \left(\forall x\left(C\subseteq D\leftrightarrow \forall y\left(y\in C\to y\in D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\right)\right)$$
27	1 25 26	e10	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\right)\right)$$
28		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
29	28	biimprcd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(y\in C\to y\in D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
30	23 27 29	e11	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)$$
31		df-ss	$$⊢⦋A/x⦌C\subseteq ⦋A/x⦌D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)$$
32		biantr	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\wedge \left(⦋A/x⦌C\subseteq ⦋A/x⦌D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow ⦋A/x⦌C\subseteq ⦋A/x⦌D\right)$$
33	32	ex	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\left(⦋A/x⦌C\subseteq ⦋A/x⦌D\leftrightarrow \forall y\left(y\in ⦋A/x⦌C\to y\in ⦋A/x⦌D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow ⦋A/x⦌C\subseteq ⦋A/x⦌D\right)\right)$$
34	30 31 33	e10	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow ⦋A/x⦌C\subseteq ⦋A/x⦌D\right)\right)$$
35	34	in1	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\subseteq D\leftrightarrow ⦋A/x⦌C\subseteq ⦋A/x⦌D\right)$$