| 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 2830 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
| 2 | 1 | anbi2d 630 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵))) |
| 3 | 2 | opabbidv 5209 | . 2 ⊢ (𝐴 = 𝐵 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}) |
| 4 | df-xp 5691 | . 2 ⊢ (𝐶 × 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} | |
| 5 | df-xp 5691 | . 2 ⊢ (𝐶 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)} | |
| 6 | 3, 4, 5 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {copab 5205 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-xp 5691 |
| This theorem is referenced by: xpeq12 5710 xpeq2i 5712 xpeq2d 5715 xpnz 6179 xpdisj2 6182 dmxpss 6191 rnxpid 6193 xpcan 6196 unixp 6302 dfpo2 6316 fconst5 7226 naddcllem 8714 pmvalg 8877 xpcomeng 9104 unxpdom 9289 marypha1 9474 djueq12 9944 dfac5lem3 10165 dfac5lem4 10166 dfac5lem4OLD 10168 hsmexlem8 10464 axdc4uz 14025 hashxp 14473 mamufval 22396 txuni2 23573 txbas 23575 txopn 23610 txrest 23639 txdis 23640 txdis1cn 23643 txtube 23648 txcmplem2 23650 tx1stc 23658 qustgplem 24129 tsmsxplem1 24161 isgrpo 30516 vciOLD 30580 isvclem 30596 issh 31227 hhssablo 31282 hhssnvt 31284 hhsssh 31288 2ndimaxp 32656 txomap 33833 tpr2rico 33911 elsx 34195 mbfmcst 34261 br2base 34271 dya2iocnrect 34283 sxbrsigalem5 34290 0rrv 34453 elima4 35776 finxpeq1 37387 isbnd3 37791 hdmap1fval 41798 csbresgVD 44915 mofeu 48757 functermc 49140 |
| Copyright terms: Public domain | W3C validator |