Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
⊢ 𝑥 ∈ V |
2 |
|
vex |
⊢ 𝑦 ∈ V |
3 |
1 2
|
opnzi |
⊢ 〈 𝑥 , 𝑦 〉 ≠ ∅ |
4 |
|
simpl |
⊢ ( ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) → ∅ = 〈 𝑥 , 𝑦 〉 ) |
5 |
4
|
eqcomd |
⊢ ( ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) → 〈 𝑥 , 𝑦 〉 = ∅ ) |
6 |
5
|
necon3ai |
⊢ ( 〈 𝑥 , 𝑦 〉 ≠ ∅ → ¬ ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
7 |
3 6
|
ax-mp |
⊢ ¬ ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) |
8 |
7
|
nex |
⊢ ¬ ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) |
9 |
8
|
nex |
⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) |
10 |
|
elopab |
⊢ ( ∅ ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
11 |
9 10
|
mtbir |
⊢ ¬ ∅ ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
12 |
|
eleq1 |
⊢ ( 〈 𝐴 , 𝐵 〉 = ∅ → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∅ ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ) |
13 |
11 12
|
mtbiri |
⊢ ( 〈 𝐴 , 𝐵 〉 = ∅ → ¬ 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
14 |
13
|
necon2ai |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → 〈 𝐴 , 𝐵 〉 ≠ ∅ ) |
15 |
|
opnz |
⊢ ( 〈 𝐴 , 𝐵 〉 ≠ ∅ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
16 |
14 15
|
sylib |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
17 |
|
sbcex |
⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐴 ∈ V ) |
18 |
|
spesbc |
⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 ) |
19 |
|
sbcex |
⊢ ( [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V ) |
20 |
19
|
exlimiv |
⊢ ( ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V ) |
21 |
18 20
|
syl |
⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V ) |
22 |
17 21
|
jca |
⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
23 |
|
opeq1 |
⊢ ( 𝑧 = 𝐴 → 〈 𝑧 , 𝑤 〉 = 〈 𝐴 , 𝑤 〉 ) |
24 |
23
|
eleq1d |
⊢ ( 𝑧 = 𝐴 → ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝐴 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ) |
25 |
|
dfsbcq2 |
⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ) |
26 |
24 25
|
bibi12d |
⊢ ( 𝑧 = 𝐴 → ( ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( 〈 𝐴 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ) ) |
27 |
|
opeq2 |
⊢ ( 𝑤 = 𝐵 → 〈 𝐴 , 𝑤 〉 = 〈 𝐴 , 𝐵 〉 ) |
28 |
27
|
eleq1d |
⊢ ( 𝑤 = 𝐵 → ( 〈 𝐴 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ) |
29 |
|
dfsbcq2 |
⊢ ( 𝑤 = 𝐵 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜑 ) ) |
30 |
29
|
sbcbidv |
⊢ ( 𝑤 = 𝐵 → ( [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) ) |
31 |
28 30
|
bibi12d |
⊢ ( 𝑤 = 𝐵 → ( ( 〈 𝐴 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) ) ) |
32 |
|
vopelopabsb |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) |
33 |
26 31 32
|
vtocl2g |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) ) |
34 |
16 22 33
|
pm5.21nii |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) |