![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.) |
Ref | Expression |
---|---|
xpeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2815 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
2 | 1 | anbi2d 628 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵))) |
3 | 2 | opabbidv 5211 | . 2 ⊢ (𝐴 = 𝐵 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}) |
4 | df-xp 5680 | . 2 ⊢ (𝐶 × 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} | |
5 | df-xp 5680 | . 2 ⊢ (𝐶 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)} | |
6 | 3, 4, 5 | 3eqtr4g 2791 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 {copab 5207 × cxp 5672 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-opab 5208 df-xp 5680 |
This theorem is referenced by: xpeq12 5699 xpeq2i 5701 xpeq2d 5704 xpnz 6162 xpdisj2 6165 dmxpss 6174 rnxpid 6176 xpcan 6179 unixp 6285 dfpo2 6299 fconst5 7215 naddcllem 8698 pmvalg 8858 xpcomeng 9094 unxpdom 9280 marypha1 9470 djueq12 9940 dfac5lem3 10161 dfac5lem4 10162 hsmexlem8 10458 axdc4uz 13998 hashxp 14446 mamufval 22380 txuni2 23557 txbas 23559 txopn 23594 txrest 23623 txdis 23624 txdis1cn 23627 txtube 23632 txcmplem2 23634 tx1stc 23642 qustgplem 24113 tsmsxplem1 24145 isgrpo 30427 vciOLD 30491 isvclem 30507 issh 31138 hhssablo 31193 hhssnvt 31195 hhsssh 31199 2ndimaxp 32564 txomap 33662 tpr2rico 33740 elsx 34040 mbfmcst 34106 br2base 34116 dya2iocnrect 34128 sxbrsigalem5 34135 0rrv 34298 elima4 35612 finxpeq1 37106 isbnd3 37498 hdmap1fval 41508 csbresgVD 44608 mofeu 48251 |
Copyright terms: Public domain | W3C validator |