| Step | Hyp | Ref
| Expression |
| 1 | | idn1 44594 |
. . . . . . . . . . . 12
⊢ ( 𝐴 ∈ 𝑉 ▶ 𝐴 ∈ 𝑉 ) |
| 2 | | sbcel12 4411 |
. . . . . . . . . . . . 13
⊢
([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵)) |
| 4 | 1, 3 | e1a 44647 |
. . . . . . . . . . 11
⊢ ( 𝐴 ∈ 𝑉 ▶ ([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 5 | | csbconstg 3918 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 = 〈𝑤, 𝑦〉) |
| 6 | 1, 5 | e1a 44647 |
. . . . . . . . . . . 12
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 = 〈𝑤, 𝑦〉 ) |
| 7 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢
(⦋𝐴 /
𝑥⦌〈𝑤, 𝑦〉 = 〈𝑤, 𝑦〉 → (⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵)) |
| 8 | 6, 7 | e1a 44647 |
. . . . . . . . . . 11
⊢ ( 𝐴 ∈ 𝑉 ▶ (⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 9 | | bibi1 351 |
. . . . . . . . . . . 12
⊢
(([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → (([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ↔ (⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
| 10 | 9 | biimprd 248 |
. . . . . . . . . . 11
⊢
(([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
| 11 | 4, 8, 10 | e11 44708 |
. . . . . . . . . 10
⊢ ( 𝐴 ∈ 𝑉 ▶ ([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 12 | 11 | gen11 44636 |
. . . . . . . . 9
⊢ ( 𝐴 ∈ 𝑉 ▶ ∀𝑤([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 13 | | exbi 1847 |
. . . . . . . . 9
⊢
(∀𝑤([𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ 〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → (∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵)) |
| 14 | 12, 13 | e1a 44647 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝑉 ▶ (∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 15 | | sbcex2 3850 |
. . . . . . . . . . 11
⊢
([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵) |
| 16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵)) |
| 17 | 16 | bicomd 223 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵)) |
| 18 | 1, 17 | e1a 44647 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝑉 ▶ (∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵) ) |
| 19 | | bitr3 352 |
. . . . . . . . 9
⊢
((∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵) → ((∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
| 20 | 19 | com12 32 |
. . . . . . . 8
⊢
((∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → ((∃𝑤[𝐴 / 𝑥]〈𝑤, 𝑦〉 ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵) → ([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
| 21 | 14, 18, 20 | e11 44708 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝑉 ▶ ([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 22 | 21 | gen11 44636 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝑉 ▶ ∀𝑦([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) ) |
| 23 | | abbib 2811 |
. . . . . . 7
⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} ↔ ∀𝑦([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵)) |
| 24 | 23 | biimpri 228 |
. . . . . 6
⊢
(∀𝑦([𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵 ↔ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵) → {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵}) |
| 25 | 22, 24 | e1a 44647 |
. . . . 5
⊢ ( 𝐴 ∈ 𝑉 ▶ {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} ) |
| 26 | | csbab 4440 |
. . . . . . 7
⊢
⦋𝐴 /
𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} |
| 27 | 26 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵}) |
| 28 | 1, 27 | e1a 44647 |
. . . . 5
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} ) |
| 29 | | eqeq2 2749 |
. . . . . 6
⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵})) |
| 30 | 29 | biimpd 229 |
. . . . 5
⊢ ({𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵})) |
| 31 | 25, 28, 30 | e11 44708 |
. . . 4
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} ) |
| 32 | | dfrn3 5900 |
. . . . . 6
⊢ ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} |
| 33 | 32 | ax-gen 1795 |
. . . . 5
⊢
∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} |
| 34 | | csbeq2 3904 |
. . . . . 6
⊢
(∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵}) |
| 35 | 34 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵})) |
| 36 | 1, 33, 35 | e10 44714 |
. . . 4
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} ) |
| 37 | | eqeq2 2749 |
. . . . 5
⊢
(⦋𝐴 /
𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵})) |
| 38 | 37 | biimpd 229 |
. . . 4
⊢
(⦋𝐴 /
𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ 𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵})) |
| 39 | 31, 36, 38 | e11 44708 |
. . 3
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} ) |
| 40 | | dfrn3 5900 |
. . 3
⊢ ran
⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} |
| 41 | | eqeq2 2749 |
. . . 4
⊢ (ran
⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 ↔ ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵})) |
| 42 | 41 | biimprcd 250 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → (ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤〈𝑤, 𝑦〉 ∈ ⦋𝐴 / 𝑥⦌𝐵} → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)) |
| 43 | 39, 40, 42 | e10 44714 |
. 2
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 ) |
| 44 | 43 | in1 44591 |
1
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) |