Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > opelxpi | Unicode version |
Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.) |
Ref | Expression |
---|---|
opelxpi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxp 4569 | . 2 | |
2 | 1 | biimpri 132 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1480 cop 3530 cxp 4537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-opab 3990 df-xp 4545 |
This theorem is referenced by: opelxpd 4572 opelvvg 4588 opelvv 4589 opbrop 4618 fliftrel 5693 fnotovb 5814 ovi3 5907 ovres 5910 fovrn 5913 fnovrn 5918 ovconst2 5922 oprab2co 6115 1stconst 6118 2ndconst 6119 f1od2 6132 brdifun 6456 ecopqsi 6484 brecop 6519 th3q 6534 xpcomco 6720 xpf1o 6738 xpmapenlem 6743 djulclr 6934 djurclr 6935 djulcl 6936 djurcl 6937 djuf1olem 6938 addpiord 7124 mulpiord 7125 enqeceq 7167 1nq 7174 addpipqqslem 7177 mulpipq 7180 mulpipqqs 7181 addclnq 7183 mulclnq 7184 recexnq 7198 ltexnqq 7216 prarloclemarch 7226 prarloclemarch2 7227 nnnq 7230 enq0breq 7244 enq0eceq 7245 nqnq0 7249 addnnnq0 7257 mulnnnq0 7258 addclnq0 7259 mulclnq0 7260 nqpnq0nq 7261 prarloclemlt 7301 prarloclemlo 7302 prarloclemcalc 7310 genpelxp 7319 nqprm 7350 ltexprlempr 7416 recexprlempr 7440 cauappcvgprlemcl 7461 cauappcvgprlemladd 7466 caucvgprlemcl 7484 caucvgprprlemcl 7512 enreceq 7544 addsrpr 7553 mulsrpr 7554 0r 7558 1sr 7559 m1r 7560 addclsr 7561 mulclsr 7562 prsrcl 7592 mappsrprg 7612 addcnsr 7642 mulcnsr 7643 addcnsrec 7650 mulcnsrec 7651 pitonnlem2 7655 pitonn 7656 pitore 7658 recnnre 7659 axaddcl 7672 axmulcl 7674 xrlenlt 7829 frecuzrdgg 10189 frecuzrdgsuctlem 10196 seq3val 10231 cnrecnv 10682 eucalgf 11736 eucalg 11740 qredeu 11778 qnumdenbi 11870 crth 11900 phimullem 11901 setscom 11999 setsslid 12009 txbas 12427 upxp 12441 uptx 12443 txlm 12448 cnmpt21 12460 txswaphmeolem 12489 txswaphmeo 12490 comet 12668 qtopbasss 12690 cnmetdval 12698 remetdval 12708 tgqioo 12716 dvcnp2cntop 12832 dvef 12856 djucllem 13007 pwle2 13193 |
Copyright terms: Public domain | W3C validator |