| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > xpeq1 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.) |
| Ref | Expression |
|---|---|
| xpeq1 | ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq2 2830 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
| 2 | 1 | anbi1d 631 | . . 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 xpeq1i 5711 xpeq1d 5714 opthprc 5749 dmxpid 5941 reseq2 5992 xpnz 6179 xpdisj1 6181 xpcan2 6197 xpima 6202 unixp 6302 unixpid 6304 naddcllem 8714 pmvalg 8877 xpsneng 9096 xpcomeng 9104 xpdom2g 9108 fodomr 9168 unxpdom 9289 xpfiOLD 9359 fodomfir 9368 marypha1lem 9473 iundom2g 10580 hashxplem 14472 dmtrclfv 15057 ramcl 17067 efgval 19735 frgpval 19776 frlmval 21768 txuni2 23573 txbas 23575 txopn 23610 txrest 23639 txdis 23640 txdis1cn 23643 tx1stc 23658 tmdgsum 24103 qustgplem 24129 incistruhgr 29096 isgrpo 30516 hhssablo 31282 hhssnvt 31284 hhsssh 31288 gsumpart 33060 txomap 33833 tpr2rico 33911 elsx 34195 br2base 34271 dya2iocnrect 34283 sxbrsigalem5 34290 sibf0 34336 cvmlift2lem13 35320 |
| Copyright terms: Public domain | W3C validator |