Theorem opelxpi 4676

Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 4674	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 133	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

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