Step | Hyp | Ref
| Expression |
1 | | vex 3417 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
2 | | vex 3417 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | opnzi 5165 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ≠
∅ |
4 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((∅
= 〈𝑥, 𝑦〉 ∧ 𝜑) → ∅ = 〈𝑥, 𝑦〉) |
5 | 4 | eqcomd 2831 |
. . . . . . . . . 10
⊢ ((∅
= 〈𝑥, 𝑦〉 ∧ 𝜑) → 〈𝑥, 𝑦〉 = ∅) |
6 | 5 | necon3ai 3024 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ≠ ∅ → ¬
(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
7 | 3, 6 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑) |
8 | 7 | nex 1899 |
. . . . . . 7
⊢ ¬
∃𝑦(∅ =
〈𝑥, 𝑦〉 ∧ 𝜑) |
9 | 8 | nex 1899 |
. . . . . 6
⊢ ¬
∃𝑥∃𝑦(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑) |
10 | | elopab 5211 |
. . . . . 6
⊢ (∅
∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(∅ = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
11 | 9, 10 | mtbir 315 |
. . . . 5
⊢ ¬
∅ ∈ {〈𝑥,
𝑦〉 ∣ 𝜑} |
12 | | eleq1 2894 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 = ∅ →
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
13 | 11, 12 | mtbiri 319 |
. . . 4
⊢
(〈𝐴, 𝐵〉 = ∅ → ¬
〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
14 | 13 | necon2ai 3028 |
. . 3
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 〈𝐴, 𝐵〉 ≠ ∅) |
15 | | opnz 5164 |
. . 3
⊢
(〈𝐴, 𝐵〉 ≠ ∅ ↔
(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
16 | 14, 15 | sylib 210 |
. 2
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
17 | | sbcex 3672 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐴 ∈ V) |
18 | | spesbc 3745 |
. . . 4
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑) |
19 | | sbcex 3672 |
. . . . 5
⊢
([𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
20 | 19 | exlimiv 2029 |
. . . 4
⊢
(∃𝑥[𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
21 | 18, 20 | syl 17 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
22 | 17, 21 | jca 507 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
23 | | opeq1 4625 |
. . . . 5
⊢ (𝑧 = 𝐴 → 〈𝑧, 𝑤〉 = 〈𝐴, 𝑤〉) |
24 | 23 | eleq1d 2891 |
. . . 4
⊢ (𝑧 = 𝐴 → (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
25 | | dfsbcq2 3665 |
. . . 4
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)) |
26 | 24, 25 | bibi12d 337 |
. . 3
⊢ (𝑧 = 𝐴 → ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑))) |
27 | | opeq2 4626 |
. . . . 5
⊢ (𝑤 = 𝐵 → 〈𝐴, 𝑤〉 = 〈𝐴, 𝐵〉) |
28 | 27 | eleq1d 2891 |
. . . 4
⊢ (𝑤 = 𝐵 → (〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
29 | | dfsbcq2 3665 |
. . . . 5
⊢ (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑 ↔ [𝐵 / 𝑦]𝜑)) |
30 | 29 | sbcbidv 3717 |
. . . 4
⊢ (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
31 | 28, 30 | bibi12d 337 |
. . 3
⊢ (𝑤 = 𝐵 → ((〈𝐴, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))) |
32 | | nfopab1 4944 |
. . . . . 6
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} |
33 | 32 | nfel2 2986 |
. . . . 5
⊢
Ⅎ𝑥〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} |
34 | | nfs1v 2311 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 |
35 | 33, 34 | nfbi 2006 |
. . . 4
⊢
Ⅎ𝑥(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
36 | | opeq1 4625 |
. . . . . 6
⊢ (𝑥 = 𝑧 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) |
37 | 36 | eleq1d 2891 |
. . . . 5
⊢ (𝑥 = 𝑧 → (〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
38 | | sbequ12 2286 |
. . . . 5
⊢ (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) |
39 | 37, 38 | bibi12d 337 |
. . . 4
⊢ (𝑥 = 𝑧 → ((〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) ↔ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))) |
40 | | nfopab2 4945 |
. . . . . . 7
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} |
41 | 40 | nfel2 2986 |
. . . . . 6
⊢
Ⅎ𝑦〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} |
42 | | nfs1v 2311 |
. . . . . 6
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
43 | 41, 42 | nfbi 2006 |
. . . . 5
⊢
Ⅎ𝑦(〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) |
44 | | opeq2 4626 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑤〉) |
45 | 44 | eleq1d 2891 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑})) |
46 | | sbequ12 2286 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑)) |
47 | 45, 46 | bibi12d 337 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) ↔ (〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑))) |
48 | | opabid 5210 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
49 | 43, 47, 48 | chvar 2415 |
. . . 4
⊢
(〈𝑥, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) |
50 | 35, 39, 49 | chvar 2415 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
51 | 26, 31, 50 | vtocl2g 3486 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
52 | 16, 22, 51 | pm5.21nii 370 |
1
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) |