Step |
Hyp |
Ref |
Expression |
1 |
|
relxp |
⊢ Rel ( { 𝑥 ∣ 𝜑 } × { 𝑦 ∣ 𝜓 } ) |
2 |
|
relopabv |
⊢ Rel { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } |
3 |
|
df-clab |
⊢ ( 𝑎 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑎 / 𝑥 ] 𝜑 ) |
4 |
|
df-clab |
⊢ ( 𝑏 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑏 / 𝑦 ] 𝜓 ) |
5 |
3 4
|
anbi12i |
⊢ ( ( 𝑎 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑏 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
6 |
|
sban |
⊢ ( [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑏 / 𝑦 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
7 |
|
sbsbc |
⊢ ( [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) |
8 |
|
sbv |
⊢ ( [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
9 |
8
|
anbi1i |
⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
10 |
6 7 9
|
3bitr3i |
⊢ ( [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
11 |
10
|
sbbii |
⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
12 |
|
sbsbc |
⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) |
13 |
|
sban |
⊢ ( [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ) |
14 |
|
sbv |
⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] 𝜓 ) |
15 |
14
|
anbi2i |
⊢ ( ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
16 |
13 15
|
bitri |
⊢ ( [ 𝑎 / 𝑥 ] ( 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
17 |
11 12 16
|
3bitr3i |
⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜑 ∧ [ 𝑏 / 𝑦 ] 𝜓 ) ) |
18 |
5 17
|
bitr4i |
⊢ ( ( 𝑎 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑏 ∈ { 𝑦 ∣ 𝜓 } ) ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) |
19 |
|
brxp |
⊢ ( 𝑎 ( { 𝑥 ∣ 𝜑 } × { 𝑦 ∣ 𝜓 } ) 𝑏 ↔ ( 𝑎 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝑏 ∈ { 𝑦 ∣ 𝜓 } ) ) |
20 |
|
eqid |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } |
21 |
20
|
brabsb |
⊢ ( 𝑎 { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } 𝑏 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) |
22 |
18 19 21
|
3bitr4i |
⊢ ( 𝑎 ( { 𝑥 ∣ 𝜑 } × { 𝑦 ∣ 𝜓 } ) 𝑏 ↔ 𝑎 { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } 𝑏 ) |
23 |
1 2 22
|
eqbrriv |
⊢ ( { 𝑥 ∣ 𝜑 } × { 𝑦 ∣ 𝜓 } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∧ 𝜓 ) } |