Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
⊢ 𝑏 ∈ V |
2 |
1
|
elima |
⊢ ( 𝑏 ∈ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑏 ) |
3 |
|
df-br |
⊢ ( 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑏 ↔ 〈 𝑧 , 𝑏 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
4 |
|
vopelopabsb |
⊢ ( 〈 𝑧 , 𝑏 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) |
5 |
3 4
|
bitri |
⊢ ( 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑏 ↔ [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) |
6 |
5
|
rexbii |
⊢ ( ∃ 𝑧 ∈ 𝐴 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } 𝑏 ↔ ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) |
7 |
|
nfs1v |
⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 |
8 |
|
nfv |
⊢ Ⅎ 𝑧 [ 𝑏 / 𝑦 ] 𝜑 |
9 |
|
sbequ12r |
⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) |
10 |
7 8 9
|
cbvrexw |
⊢ ( ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 ) |
11 |
2 6 10
|
3bitri |
⊢ ( 𝑏 ∈ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 ) |