Theorem sbcssgVD 41224

Description: Virtual deduction proof of sbcssg 4465. 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 4465 is sbcssgVD 41224 without virtual deductions and was automatically derived from sbcssgVD 41224.

1::	⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
3:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)   )
4:2,3:	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷 ))   )
5:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷))   )
6:4,5:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
7:6:	⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
8:7:	⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) )   )
9:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))   )
10:8,9:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) )   )
11::	⊢ (𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
110:11:	⊢ ∀𝑥(𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
12:1,110:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))   )
13:10,12:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
14::	⊢ (⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀ 𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))
15:13,14:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)   )
qed:15:	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋ 𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
sbcssgVD	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷))

Proof of Theorem sbcssgVD

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 40915	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		sbcel2 4369	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
3	2	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
4	1, 3	e1a 40968	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
5		sbcel2 4369	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)
6	5	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))
7	1, 6	e1a 40968	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)   )
8		imbi12 349	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) → (([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
9	4, 7, 8	e11 41029	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
10		sbcimg 3822	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)))
11	1, 10	e1a 40968	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷))   )
12		bibi1 354	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
13	12	biimprcd 252	. . . . . . . 8 ⊢ ((([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
14	9, 11, 13	e11 41029	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
15	14	gen11 40957	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
16		albi 1819	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))
17	15, 16	e1a 40968	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
18		sbcal 3835	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
19	18	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)))
20	1, 19	e1a 40968	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))   )
21		bibi1 354	. . . . . 6 ⊢ (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
22	21	biimprcd 252	. . . . 5 ⊢ ((∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
23	17, 20, 22	e11 41029	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
24		dfss2 3957	. . . . . 6 ⊢ (𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
25	24	ax-gen 1796	. . . . 5 ⊢ ∀𝑥(𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
26		sbcbi 40880	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))))
27	1, 25, 26	e10 41035	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))   )
28		bibi1 354	. . . . 5 ⊢ (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
29	28	biimprcd 252	. . . 4 ⊢ (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
30	23, 27, 29	e11 41029	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
31		dfss2 3957	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))
32		biantr 804	. . . 4 ⊢ ((([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ∧ (⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷))
33	32	ex 415	. . 3 ⊢ (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ((⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)))
34	30, 31, 33	e10 41035	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)   )
35	34	in1 40912	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  [wsbc 3774  ⦋csb 3885   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294  df-vd1 40911

This theorem is referenced by: (None)