![]() |
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 4671 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpri 133 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4189 ax-pr 4224 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-opab 4080 df-xp 4647 |
This theorem is referenced by: opelxpd 4674 opelvvg 4690 opelvv 4691 opbrop 4720 fliftrel 5809 fnotovb 5934 ovi3 6028 ovres 6031 fovcdm 6034 fnovrn 6039 ovconst2 6043 oprab2co 6237 1stconst 6240 2ndconst 6241 f1od2 6254 brdifun 6580 ecopqsi 6608 brecop 6643 th3q 6658 xpcomco 6844 xpf1o 6862 xpmapenlem 6867 djulclr 7066 djurclr 7067 djulcl 7068 djurcl 7069 djuf1olem 7070 cc2lem 7283 addpiord 7333 mulpiord 7334 enqeceq 7376 1nq 7383 addpipqqslem 7386 mulpipq 7389 mulpipqqs 7390 addclnq 7392 mulclnq 7393 recexnq 7407 ltexnqq 7425 prarloclemarch 7435 prarloclemarch2 7436 nnnq 7439 enq0breq 7453 enq0eceq 7454 nqnq0 7458 addnnnq0 7466 mulnnnq0 7467 addclnq0 7468 mulclnq0 7469 nqpnq0nq 7470 prarloclemlt 7510 prarloclemlo 7511 prarloclemcalc 7519 genpelxp 7528 nqprm 7559 ltexprlempr 7625 recexprlempr 7649 cauappcvgprlemcl 7670 cauappcvgprlemladd 7675 caucvgprlemcl 7693 caucvgprprlemcl 7721 enreceq 7753 addsrpr 7762 mulsrpr 7763 0r 7767 1sr 7768 m1r 7769 addclsr 7770 mulclsr 7771 prsrcl 7801 mappsrprg 7821 addcnsr 7851 mulcnsr 7852 addcnsrec 7859 mulcnsrec 7860 pitonnlem2 7864 pitonn 7865 pitore 7867 recnnre 7868 axaddcl 7881 axmulcl 7883 xrlenlt 8040 frecuzrdgg 10434 frecuzrdgsuctlem 10441 seq3val 10476 cnrecnv 10937 eucalgf 12073 eucalg 12077 qredeu 12115 qnumdenbi 12210 crth 12242 phimullem 12243 setscom 12520 setsslid 12531 imasaddfnlemg 12757 imasaddflemg 12759 txbas 14155 upxp 14169 uptx 14171 txlm 14176 cnmpt21 14188 txswaphmeolem 14217 txswaphmeo 14218 comet 14396 qtopbasss 14418 cnmetdval 14426 remetdval 14436 tgqioo 14444 dvcnp2cntop 14560 dvef 14585 djucllem 14949 pwle2 15146 |
Copyright terms: Public domain | W3C validator |