Step | Hyp | Ref
| Expression |
1 | | vex 3479 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
2 | | vex 3479 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 1, 2 | opnzi 5475 |
. . . . . . . . 9
⊢
⟨𝑥, 𝑦⟩ ≠
∅ |
4 | | simpl 484 |
. . . . . . . . . . 11
⊢ ((∅
= ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∅ = ⟨𝑥, 𝑦⟩) |
5 | 4 | eqcomd 2739 |
. . . . . . . . . 10
⊢ ((∅
= ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ⟨𝑥, 𝑦⟩ = ∅) |
6 | 5 | necon3ai 2966 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ≠ ∅ → ¬
(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
7 | 3, 6 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) |
8 | 7 | nex 1803 |
. . . . . . 7
⊢ ¬
∃𝑦(∅ =
⟨𝑥, 𝑦⟩ ∧ 𝜑) |
9 | 8 | nex 1803 |
. . . . . 6
⊢ ¬
∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) |
10 | | elopab 5528 |
. . . . . 6
⊢ (∅
∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
11 | 9, 10 | mtbir 323 |
. . . . 5
⊢ ¬
∅ ∈ {⟨𝑥,
𝑦⟩ ∣ 𝜑} |
12 | | eleq1 2822 |
. . . . 5
⊢
(⟨𝐴, 𝐵⟩ = ∅ →
(⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})) |
13 | 11, 12 | mtbiri 327 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ = ∅ → ¬
⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) |
14 | 13 | necon2ai 2971 |
. . 3
⊢
(⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ⟨𝐴, 𝐵⟩ ≠ ∅) |
15 | | opnz 5474 |
. . 3
⊢
(⟨𝐴, 𝐵⟩ ≠ ∅ ↔
(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
16 | 14, 15 | sylib 217 |
. 2
⊢
(⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
17 | | sbcex 3788 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐴 ∈ V) |
18 | | spesbc 3877 |
. . . 4
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → ∃𝑥[𝐵 / 𝑦]𝜑) |
19 | | sbcex 3788 |
. . . . 5
⊢
([𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
20 | 19 | exlimiv 1934 |
. . . 4
⊢
(∃𝑥[𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
21 | 18, 20 | syl 17 |
. . 3
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐵 ∈ V) |
22 | 17, 21 | jca 513 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
23 | | opeq1 4874 |
. . . . 5
⊢ (𝑧 = 𝐴 → ⟨𝑧, 𝑤⟩ = ⟨𝐴, 𝑤⟩) |
24 | 23 | eleq1d 2819 |
. . . 4
⊢ (𝑧 = 𝐴 → (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})) |
25 | | dfsbcq2 3781 |
. . . 4
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑)) |
26 | 24, 25 | bibi12d 346 |
. . 3
⊢ (𝑧 = 𝐴 → ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑))) |
27 | | opeq2 4875 |
. . . . 5
⊢ (𝑤 = 𝐵 → ⟨𝐴, 𝑤⟩ = ⟨𝐴, 𝐵⟩) |
28 | 27 | eleq1d 2819 |
. . . 4
⊢ (𝑤 = 𝐵 → (⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})) |
29 | | dfsbcq2 3781 |
. . . . 5
⊢ (𝑤 = 𝐵 → ([𝑤 / 𝑦]𝜑 ↔ [𝐵 / 𝑦]𝜑)) |
30 | 29 | sbcbidv 3837 |
. . . 4
⊢ (𝑤 = 𝐵 → ([𝐴 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
31 | 28, 30 | bibi12d 346 |
. . 3
⊢ (𝑤 = 𝐵 → ((⟨𝐴, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑))) |
32 | | vopelopabsb 5530 |
. . 3
⊢
(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
33 | 26, 31, 32 | vtocl2g 3563 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
34 | 16, 22, 33 | pm5.21nii 380 |
1
⊢
(⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) |