![]() |
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 4527 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
2 | 1 | biimpri 132 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1461 〈cop 3494 × cxp 4495 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-pow 4056 ax-pr 4089 |
This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ral 2393 df-rex 2394 df-v 2657 df-un 3039 df-in 3041 df-ss 3048 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 df-opab 3948 df-xp 4503 |
This theorem is referenced by: opelxpd 4530 opelvvg 4546 opelvv 4547 opbrop 4576 fliftrel 5645 fnotovb 5766 ovi3 5859 ovres 5862 fovrn 5865 fnovrn 5870 ovconst2 5874 oprab2co 6066 1stconst 6069 2ndconst 6070 f1od2 6083 brdifun 6407 ecopqsi 6435 brecop 6470 th3q 6485 xpcomco 6670 xpf1o 6688 xpmapenlem 6693 djulclr 6883 djurclr 6884 djulcl 6885 djurcl 6886 djuf1olem 6887 addpiord 7065 mulpiord 7066 enqeceq 7108 1nq 7115 addpipqqslem 7118 mulpipq 7121 mulpipqqs 7122 addclnq 7124 mulclnq 7125 recexnq 7139 ltexnqq 7157 prarloclemarch 7167 prarloclemarch2 7168 nnnq 7171 enq0breq 7185 enq0eceq 7186 nqnq0 7190 addnnnq0 7198 mulnnnq0 7199 addclnq0 7200 mulclnq0 7201 nqpnq0nq 7202 prarloclemlt 7242 prarloclemlo 7243 prarloclemcalc 7251 genpelxp 7260 nqprm 7291 ltexprlempr 7357 recexprlempr 7381 cauappcvgprlemcl 7402 cauappcvgprlemladd 7407 caucvgprlemcl 7425 caucvgprprlemcl 7453 enreceq 7472 addsrpr 7481 mulsrpr 7482 0r 7486 1sr 7487 m1r 7488 addclsr 7489 mulclsr 7490 prsrcl 7519 addcnsr 7562 mulcnsr 7563 addcnsrec 7570 mulcnsrec 7571 pitonnlem2 7575 pitonn 7576 pitore 7578 recnnre 7579 axaddcl 7592 axmulcl 7594 xrlenlt 7746 frecuzrdgg 10075 frecuzrdgsuctlem 10082 seq3val 10117 cnrecnv 10568 eucalgf 11575 eucalg 11579 qredeu 11617 qnumdenbi 11708 crth 11738 phimullem 11739 setscom 11835 setsslid 11845 txbas 12262 upxp 12276 uptx 12278 txlm 12283 cnmpt21 12295 comet 12481 qtopbasss 12503 cnmetdval 12511 remetdval 12518 tgqioo 12526 dvcnp2cntop 12611 djucllem 12686 pwle2 12872 |
Copyright terms: Public domain | W3C validator |