Theorem opelxpi 4673

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

Assertion

Ref	Expression
opelxpi	|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 4671	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2	1	biimpri 133	1 |- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2160   <.cop 3610   X. cxp 4639

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