Step | Hyp | Ref
| Expression |
1 | | idn1 38790 |
. . . . . . . . . 10
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
2 | | sbcel2gOLD 38755 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
3 | 1, 2 | e1a 38852 |
. . . . . . . . 9
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) ) |
4 | | sbcel2gOLD 38755 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) |
5 | 1, 4 | e1a 38852 |
. . . . . . . . 9
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) ) |
6 | | imbi12 336 |
. . . . . . . . 9
⊢
(([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) → (([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
7 | 3, 5, 6 | e11 38913 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝐵 ▶ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
8 | | sbcimg 3477 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷))) |
9 | 1, 8 | e1a 38852 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)) ) |
10 | | bibi1 341 |
. . . . . . . . 9
⊢
(([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
11 | 10 | biimprcd 240 |
. . . . . . . 8
⊢
((([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 → [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
12 | 7, 9, 11 | e11 38913 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
13 | 12 | gen11 38841 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 ▶ ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
14 | | albi 1746 |
. . . . . 6
⊢
(∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))) |
15 | 13, 14 | e1a 38852 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 ▶ (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
16 | | sbcalgOLD 38752 |
. . . . . 6
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))) |
17 | 1, 16 | e1a 38852 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) ) |
18 | | bibi1 341 |
. . . . . 6
⊢
(([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
19 | 18 | biimprcd 240 |
. . . . 5
⊢
((∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
20 | 15, 17, 19 | e11 38913 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
21 | | dfss2 3591 |
. . . . . 6
⊢ (𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) |
22 | 21 | ax-gen 1722 |
. . . . 5
⊢
∀𝑥(𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) |
23 | | sbcbi 38749 |
. . . . 5
⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)))) |
24 | 1, 22, 23 | e10 38919 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) ) |
25 | | bibi1 341 |
. . . . 5
⊢
(([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ ([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
26 | 25 | biimprcd 240 |
. . . 4
⊢
(([𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷) ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ [𝐴 / 𝑥]∀𝑦(𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))) |
27 | 20, 24, 26 | e11 38913 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ) |
28 | | dfss2 3591 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) |
29 | | biantr 972 |
. . . 4
⊢
((([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ∧ (⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) |
30 | 29 | ex 450 |
. . 3
⊢
(([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ((⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ ∀𝑦(𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 → 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷))) |
31 | 27, 28, 30 | e10 38919 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷) ) |
32 | 31 | in1 38787 |
1
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) |