![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opeq12 | GIF version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
Ref | Expression |
---|---|
opeq12 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 3644 | . 2 ⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) | |
2 | opeq2 3645 | . 2 ⊢ (𝐵 = 𝐷 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) | |
3 | 1, 2 | sylan9eq 2147 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1296 〈cop 3469 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 |
This theorem is referenced by: opeq12i 3649 opeq12d 3652 cbvopab 3931 opth 4088 copsex2t 4096 copsex2g 4097 relop 4617 funopg 5082 fsn 5508 fnressn 5522 cbvoprab12 5760 eqopi 5980 f1o2ndf1 6031 tposoprab 6083 brecop 6422 th3q 6437 ecovcom 6439 ecovicom 6440 ecovass 6441 ecoviass 6442 ecovdi 6443 ecovidi 6444 xpf1o 6640 1qec 7044 enq0sym 7088 addnq0mo 7103 mulnq0mo 7104 addnnnq0 7105 mulnnnq0 7106 distrnq0 7115 mulcomnq0 7116 addassnq0 7118 addsrmo 7386 mulsrmo 7387 addsrpr 7388 mulsrpr 7389 axcnre 7513 fsumcnv 10995 eucalgval2 11477 |
Copyright terms: Public domain | W3C validator |