Step |
Hyp |
Ref |
Expression |
1 |
|
bj-1upleq |
⊢ ( 𝐴 = 𝐵 → ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ ) |
2 |
|
bj-xtageq |
⊢ ( 𝐶 = 𝐷 → ( { 1o } × tag 𝐶 ) = ( { 1o } × tag 𝐷 ) ) |
3 |
|
uneq12 |
⊢ ( ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ ∧ ( { 1o } × tag 𝐶 ) = ( { 1o } × tag 𝐷 ) ) → ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐶 ) ) = ( ⦅ 𝐵 ⦆ ∪ ( { 1o } × tag 𝐷 ) ) ) |
4 |
3
|
ex |
⊢ ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ → ( ( { 1o } × tag 𝐶 ) = ( { 1o } × tag 𝐷 ) → ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐶 ) ) = ( ⦅ 𝐵 ⦆ ∪ ( { 1o } × tag 𝐷 ) ) ) ) |
5 |
1 2 4
|
syl2im |
⊢ ( 𝐴 = 𝐵 → ( 𝐶 = 𝐷 → ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐶 ) ) = ( ⦅ 𝐵 ⦆ ∪ ( { 1o } × tag 𝐷 ) ) ) ) |
6 |
|
df-bj-2upl |
⊢ ⦅ 𝐴 , 𝐶 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐶 ) ) |
7 |
|
df-bj-2upl |
⊢ ⦅ 𝐵 , 𝐷 ⦆ = ( ⦅ 𝐵 ⦆ ∪ ( { 1o } × tag 𝐷 ) ) |
8 |
6 7
|
eqeq12i |
⊢ ( ⦅ 𝐴 , 𝐶 ⦆ = ⦅ 𝐵 , 𝐷 ⦆ ↔ ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐶 ) ) = ( ⦅ 𝐵 ⦆ ∪ ( { 1o } × tag 𝐷 ) ) ) |
9 |
5 8
|
syl6ibr |
⊢ ( 𝐴 = 𝐵 → ( 𝐶 = 𝐷 → ⦅ 𝐴 , 𝐶 ⦆ = ⦅ 𝐵 , 𝐷 ⦆ ) ) |