| 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 2855 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
| 2 | 1 | anbi2d 642 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵))) |
| 3 | 2 | opabbidv 5180 | . 2 ⊢ (𝐴 = 𝐵 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}) |
| 4 | df-xp 5670 | . 2 ⊢ (𝐶 × 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} | |
| 5 | df-xp 5670 | . 2 ⊢ (𝐶 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)} | |
| 6 | 3, 4, 5 | 3eqtr4g 2826 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 {copab 5176 × cxp 5662 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2738 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-sb 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-opab 5177 df-xp 5670 |
| This theorem is used by: xpeq12 5689 xpeq2i 5691 xpeq2d 5694 xpnz 6159 xpdisj2 6162 dmxpss 6172 rnxpid 6174 xpcan 6177 unixp 6287 dfpo2 6301 fconst5 7208 naddcllem 8664 pmvalg 8836 xpcomeng 9059 unxpdom 9221 marypha1 9396 djueq12 9901 dfac5lem3 10120 dfac5lem4 10121 hsmexlem8 10418 axdc4uz 14031 hashxp 14482 mamufval 22564 txuni2 23737 txbas 23739 txopn 23774 txrest 23803 txdis 23804 txdis1cn 23807 txtube 23812 txcmplem2 23814 tx1stc 23822 qustgplem 24293 tsmsxplem1 24325 isgrpo 30864 vciOLD 30928 isvclem 30944 issh 31575 hhssablo 31630 hhssnvt 31632 hhsssh 31636 2ndimaxp 33006 txomap 34237 tpr2rico 34315 elsx 34597 mbfmcst 34662 br2base 34672 dya2iocnrect 34684 sxbrsigalem5 34691 0rrv 34854 elima4 36280 finxpeq1 38064 isbnd3 38467 hdmap1fval 42602 csbresgVD 45635 mofeu 49658 functermc 50318 |
| Copyright terms: Public domain | W3C validator |