Step | Hyp | Ref
| Expression |
1 | | df-br 4641 |
. . 3
⊢ (A{⟨x, y⟩ ∣ φ}B
↔ ⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ}) |
2 | | brex 4690 |
. . 3
⊢ (A{⟨x, y⟩ ∣ φ}B
→ (A ∈ V ∧ B ∈
V)) |
3 | 1, 2 | sylbir 204 |
. 2
⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} → (A ∈ V ∧ B ∈ V)) |
4 | | sbcex 3056 |
. . 3
⊢ ([̣A / x]̣[̣B
/ y]̣φ → A ∈
V) |
5 | | spesbc 3128 |
. . . 4
⊢ ([̣A / x]̣[̣B
/ y]̣φ → ∃x[̣B /
y]̣φ) |
6 | | sbcex 3056 |
. . . . 5
⊢ ([̣B / y]̣φ
→ B ∈ V) |
7 | 6 | exlimiv 1634 |
. . . 4
⊢ (∃x[̣B /
y]̣φ → B ∈
V) |
8 | 5, 7 | syl 15 |
. . 3
⊢ ([̣A / x]̣[̣B
/ y]̣φ → B ∈
V) |
9 | 4, 8 | jca 518 |
. 2
⊢ ([̣A / x]̣[̣B
/ y]̣φ → (A ∈ V ∧ B ∈ V)) |
10 | | opeq1 4579 |
. . . . 5
⊢ (z = A →
⟨z,
w⟩ =
⟨A,
w⟩) |
11 | 10 | eleq1d 2419 |
. . . 4
⊢ (z = A →
(⟨z,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ⟨A, w⟩ ∈ {⟨x, y⟩ ∣ φ})) |
12 | | dfsbcq2 3050 |
. . . 4
⊢ (z = A →
([z / x][w / y]φ ↔
[̣A / x]̣[w /
y]φ)) |
13 | 11, 12 | bibi12d 312 |
. . 3
⊢ (z = A →
((⟨z,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ) ↔ (⟨A, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[w /
y]φ))) |
14 | | opeq2 4580 |
. . . . 5
⊢ (w = B →
⟨A,
w⟩ =
⟨A,
B⟩) |
15 | 14 | eleq1d 2419 |
. . . 4
⊢ (w = B →
(⟨A,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ})) |
16 | | dfsbcq2 3050 |
. . . . 5
⊢ (w = B →
([w / y]φ ↔
[̣B / y]̣φ)) |
17 | 16 | sbcbidv 3101 |
. . . 4
⊢ (w = B →
([̣A / x]̣[w /
y]φ
↔ [̣A / x]̣[̣B
/ y]̣φ)) |
18 | 15, 17 | bibi12d 312 |
. . 3
⊢ (w = B →
((⟨A,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[w /
y]φ) ↔ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[̣B
/ y]̣φ))) |
19 | | nfopab1 4629 |
. . . . . 6
⊢
Ⅎx{⟨x, y⟩ ∣ φ} |
20 | 19 | nfel2 2502 |
. . . . 5
⊢ Ⅎx⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ} |
21 | | nfs1v 2106 |
. . . . 5
⊢ Ⅎx[z / x][w / y]φ |
22 | 20, 21 | nfbi 1834 |
. . . 4
⊢ Ⅎx(⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ}
↔ [z / x][w / y]φ) |
23 | | opeq1 4579 |
. . . . . 6
⊢ (x = z →
⟨x,
w⟩ =
⟨z,
w⟩) |
24 | 23 | eleq1d 2419 |
. . . . 5
⊢ (x = z →
(⟨x,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ})) |
25 | | sbequ12 1919 |
. . . . 5
⊢ (x = z →
([w / y]φ ↔
[z / x][w / y]φ)) |
26 | 24, 25 | bibi12d 312 |
. . . 4
⊢ (x = z →
((⟨x,
w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [w / y]φ) ↔ (⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ))) |
27 | | nfopab2 4630 |
. . . . . . 7
⊢
Ⅎy{⟨x, y⟩ ∣ φ} |
28 | 27 | nfel2 2502 |
. . . . . 6
⊢ Ⅎy⟨x, w⟩ ∈ {⟨x, y⟩ ∣ φ} |
29 | | nfs1v 2106 |
. . . . . 6
⊢ Ⅎy[w / y]φ |
30 | 28, 29 | nfbi 1834 |
. . . . 5
⊢ Ⅎy(⟨x, w⟩ ∈ {⟨x, y⟩ ∣ φ}
↔ [w / y]φ) |
31 | | opeq2 4580 |
. . . . . . 7
⊢ (y = w →
⟨x,
y⟩ =
⟨x,
w⟩) |
32 | 31 | eleq1d 2419 |
. . . . . 6
⊢ (y = w →
(⟨x,
y⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ⟨x, w⟩ ∈ {⟨x, y⟩ ∣ φ})) |
33 | | sbequ12 1919 |
. . . . . 6
⊢ (y = w →
(φ ↔ [w / y]φ)) |
34 | 32, 33 | bibi12d 312 |
. . . . 5
⊢ (y = w →
((⟨x,
y⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ φ) ↔ (⟨x, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [w / y]φ))) |
35 | | opabid 4696 |
. . . . 5
⊢ (⟨x, y⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ φ) |
36 | 30, 34, 35 | chvar 1986 |
. . . 4
⊢ (⟨x, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [w / y]φ) |
37 | 22, 26, 36 | chvar 1986 |
. . 3
⊢ (⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ) |
38 | 13, 18, 37 | vtocl2g 2919 |
. 2
⊢ ((A ∈ V ∧ B ∈ V) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[̣B
/ y]̣φ)) |
39 | 3, 9, 38 | pm5.21nii 342 |
1
⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[̣B
/ y]̣φ) |