![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.) |
Ref | Expression |
---|---|
xpeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2518 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi2d 710 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | opabbidv 4466 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-xp 4840 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-xp 4840 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3eqtr4g 2510 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-opab 4462 df-xp 4840 |
This theorem is referenced by: xpeq12 4853 xpeq2i 4855 xpeq2d 4858 xpnz 5256 xpdisj2 5259 dmxpss 5268 rnxpid 5270 xpcan 5273 unixp 5369 fconst5 6122 pmvalg 7483 xpcomeng 7664 unxpdom 7779 marypha1 7948 dfac5lem3 8556 dfac5lem4 8557 hsmexlem8 8854 axdc4uz 12196 hashxp 12606 mamufval 19410 txuni2 20580 txbas 20582 txopn 20617 txrest 20646 txdis 20647 txdis1cn 20650 txtube 20655 txcmplem2 20657 tx1stc 20665 qustgplem 21135 tsmsxplem1 21167 isgrpo 25924 vci 26167 isvclem 26196 vcoprnelem 26197 issh 26861 hhssablo 26914 hhssnvt 26916 hhsssh 26920 txomap 28661 tpr2rico 28718 elsx 29016 mbfmcst 29081 br2base 29091 dya2iocnrect 29103 sxbrsigalem5 29110 0rrv 29284 ghomgrplem 30307 dfpo2 30395 elima4 30421 finxpeq1 31778 isbnd3 32116 hdmap1fval 35365 csbresgVD 37292 |
Copyright terms: Public domain | W3C validator |