Step | Hyp | Ref
| Expression |
1 | | vex 3498 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
2 | | vex 3498 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | opnzi 5359 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ≠
∅ |
4 | | simpl 485 |
. . . . . . . . . . 11
⊢ ((∅
= 〈𝑥, 𝑦〉 ∧ 𝜑) → ∅ = 〈𝑥, 𝑦〉) |
5 | 4 | eqcomd 2827 |
. . . . . . . . . 10
⊢ ((∅
= 〈𝑥, 𝑦〉 ∧ 𝜑) → 〈𝑥, 𝑦〉 = ∅) |
6 | 5 | necon3ai 3041 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ≠ ∅ → ¬
(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
7 | 3, 6 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑) |
8 | 7 | nex 1797 |
. . . . . . 7
⊢ ¬
∃𝑦(∅ =
〈𝑥, 𝑦〉 ∧ 𝜑) |
9 | 8 | nex 1797 |
. . . . . 6
⊢ ¬
∃𝑥∃𝑦(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑) |
10 | | elopab 5407 |
. . . . . 6
⊢ (∅
∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
11 | 9, 10 | mtbir 325 |
. . . . 5
⊢ ¬
∅ ∈ {〈𝑥,
𝑦〉 ∣ 𝜑} |
12 | | eleq1 2900 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 = ∅ →
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
13 | 11, 12 | mtbiri 329 |
. . . 4
⊢
(〈𝐴, 𝐵〉 = ∅ → ¬
〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
14 | 13 | necon2ai 3045 |
. . 3
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 〈𝐴, 𝐵〉 ≠ ∅) |
15 | | opnz 5358 |
. . 3
⊢
(〈𝐴, 𝐵〉 ≠ ∅ ↔
(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
16 | 14, 15 | sylib 220 |
. 2
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
17 | | sbcex 3782 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐴 ∈ V) |
18 | | spesbc 3865 |
. . . 4
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑) |
19 | | sbcex 3782 |
. . . . 5
⊢
([𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
20 | 19 | exlimiv 1927 |
. . . 4
⊢
(∃𝑥[𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
21 | 18, 20 | syl 17 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
22 | 17, 21 | jca 514 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
23 | | opeq1 4797 |
. . . . 5
⊢ (𝑧 = 𝐴 → 〈𝑧, 𝑤〉 = 〈𝐴, 𝑤〉) |
24 | 23 | eleq1d 2897 |
. . . 4
⊢ (𝑧 = 𝐴 → (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
25 | | dfsbcq2 3775 |
. . . 4
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)) |
26 | 24, 25 | bibi12d 348 |
. . 3
⊢ (𝑧 = 𝐴 → ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑))) |
27 | | opeq2 4798 |
. . . . 5
⊢ (𝑤 = 𝐵 → 〈𝐴, 𝑤〉 = 〈𝐴, 𝐵〉) |
28 | 27 | eleq1d 2897 |
. . . 4
⊢ (𝑤 = 𝐵 → (〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
29 | | dfsbcq2 3775 |
. . . . 5
⊢ (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑 ↔ [𝐵 / 𝑦]𝜑)) |
30 | 29 | sbcbidv 3827 |
. . . 4
⊢ (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
31 | 28, 30 | bibi12d 348 |
. . 3
⊢ (𝑤 = 𝐵 → ((〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))) |
32 | | nfopab1 5128 |
. . . . . 6
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} |
33 | 32 | nfel2 2996 |
. . . . 5
⊢
Ⅎ𝑥〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} |
34 | | nfs1v 2269 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
35 | 33, 34 | nfbi 1900 |
. . . 4
⊢
Ⅎ𝑥(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
36 | | opeq1 4797 |
. . . . . 6
⊢ (𝑥 = 𝑧 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) |
37 | 36 | eleq1d 2897 |
. . . . 5
⊢ (𝑥 = 𝑧 → (〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
38 | | sbequ12 2248 |
. . . . 5
⊢ (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) |
39 | 37, 38 | bibi12d 348 |
. . . 4
⊢ (𝑥 = 𝑧 → ((〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) ↔ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))) |
40 | | nfopab2 5129 |
. . . . . . 7
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} |
41 | 40 | nfel2 2996 |
. . . . . 6
⊢
Ⅎ𝑦〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} |
42 | | nfs1v 2269 |
. . . . . 6
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
43 | 41, 42 | nfbi 1900 |
. . . . 5
⊢
Ⅎ𝑦(〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) |
44 | | opeq2 4798 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑤〉) |
45 | 44 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
46 | | sbequ12 2248 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑)) |
47 | 45, 46 | bibi12d 348 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) ↔ (〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑))) |
48 | | opabidw 5405 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
49 | 43, 47, 48 | chvarfv 2237 |
. . . 4
⊢
(〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) |
50 | 35, 39, 49 | chvarfv 2237 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
51 | 26, 31, 50 | vtocl2g 3572 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
52 | 16, 22, 51 | pm5.21nii 382 |
1
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) |