![]() |
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 2848 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) | |
2 | 1 | anbi2d 622 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵))) |
3 | 2 | opabbidv 4952 | . 2 ⊢ (𝐴 = 𝐵 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}) |
4 | df-xp 5361 | . 2 ⊢ (𝐶 × 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} | |
5 | df-xp 5361 | . 2 ⊢ (𝐶 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)} | |
6 | 3, 4, 5 | 3eqtr4g 2839 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∈ wcel 2107 {copab 4948 × cxp 5353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-opab 4949 df-xp 5361 |
This theorem is referenced by: xpeq12 5380 xpeq2i 5382 xpeq2d 5385 xpnz 5807 xpdisj2 5810 dmxpss 5819 rnxpid 5821 xpcan 5824 unixp 5922 fconst5 6743 pmvalg 8151 xpcomeng 8340 unxpdom 8455 marypha1 8628 djueq12 9064 dfac5lem3 9281 dfac5lem4 9282 hsmexlem8 9581 axdc4uz 13102 hashxp 13535 mamufval 20595 txuni2 21777 txbas 21779 txopn 21814 txrest 21843 txdis 21844 txdis1cn 21847 txtube 21852 txcmplem2 21854 tx1stc 21862 qustgplem 22332 tsmsxplem1 22364 isgrpo 27924 vciOLD 27988 isvclem 28004 issh 28637 hhssablo 28692 hhssnvt 28694 hhsssh 28698 txomap 30499 tpr2rico 30556 elsx 30855 mbfmcst 30919 br2base 30929 dya2iocnrect 30941 sxbrsigalem5 30948 0rrv 31112 dfpo2 32239 elima4 32267 finxpeq1 33818 isbnd3 34207 hdmap1fval 37950 csbresgVD 40064 |
Copyright terms: Public domain | W3C validator |