Metamath Proof Explorer

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 .

1:: |- (. A e. B ->. A e. B ).
2:1: |- (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
3:1: |- (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
4:2,3: |- (. A e. B ->. ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
5:1: |- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) ).
6:4,5: |- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
7:6: |- (. A e. B ->. A. y ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
8:7: |- (. A e. B ->. ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
9:1: |- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) ).
10:8,9: |- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
11:: |- ( C C_ D <-> A. y ( y e. C -> y e. D ) )
110:11: |- A. x ( C C_ D <-> A. y ( y e. C -> y e. D ) )
12:1,110: |- (. A e. B ->. ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) ).
13:10,12: |- (. A e. B ->. ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
14:: |- ( [_ A / x ]_ C C_ [_ A / x ]_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) )
15:13,14: |- (. A e. B ->. ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) ).
qed:15: |- ( A e. B -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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