![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opelxpi | GIF 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 4674 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
2 | 1 | biimpri 133 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2160 〈cop 3610 × cxp 4642 |
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 4192 ax-pr 4227 |
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 4650 |
This theorem is referenced by: opelxpd 4677 opelvvg 4693 opelvv 4694 opbrop 4723 fliftrel 5814 fnotovb 5940 ovi3 6034 ovres 6037 fovcdm 6040 fnovrn 6045 ovconst2 6049 oprab2co 6244 1stconst 6247 2ndconst 6248 f1od2 6261 brdifun 6587 ecopqsi 6617 brecop 6652 th3q 6667 xpcomco 6853 xpf1o 6873 xpmapenlem 6878 djulclr 7079 djurclr 7080 djulcl 7081 djurcl 7082 djuf1olem 7083 cc2lem 7296 addpiord 7346 mulpiord 7347 enqeceq 7389 1nq 7396 addpipqqslem 7399 mulpipq 7402 mulpipqqs 7403 addclnq 7405 mulclnq 7406 recexnq 7420 ltexnqq 7438 prarloclemarch 7448 prarloclemarch2 7449 nnnq 7452 enq0breq 7466 enq0eceq 7467 nqnq0 7471 addnnnq0 7479 mulnnnq0 7480 addclnq0 7481 mulclnq0 7482 nqpnq0nq 7483 prarloclemlt 7523 prarloclemlo 7524 prarloclemcalc 7532 genpelxp 7541 nqprm 7572 ltexprlempr 7638 recexprlempr 7662 cauappcvgprlemcl 7683 cauappcvgprlemladd 7688 caucvgprlemcl 7706 caucvgprprlemcl 7734 enreceq 7766 addsrpr 7775 mulsrpr 7776 0r 7780 1sr 7781 m1r 7782 addclsr 7783 mulclsr 7784 prsrcl 7814 mappsrprg 7834 addcnsr 7864 mulcnsr 7865 addcnsrec 7872 mulcnsrec 7873 pitonnlem2 7877 pitonn 7878 pitore 7880 recnnre 7881 axaddcl 7894 axmulcl 7896 xrlenlt 8053 frecuzrdgg 10449 frecuzrdgsuctlem 10456 seq3val 10491 cnrecnv 10954 eucalgf 12090 eucalg 12094 qredeu 12132 qnumdenbi 12227 crth 12259 phimullem 12260 setscom 12555 setsslid 12566 imasaddfnlemg 12794 imasaddflemg 12796 txbas 14235 upxp 14249 uptx 14251 txlm 14256 cnmpt21 14268 txswaphmeolem 14297 txswaphmeo 14298 comet 14476 qtopbasss 14498 cnmetdval 14506 remetdval 14516 tgqioo 14524 dvcnp2cntop 14640 dvef 14665 djucllem 15030 pwle2 15227 |
Copyright terms: Public domain | W3C validator |