Theorem opelxpi 4783

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 4781	. 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 2205   <.cop 3694   X. cxp 4749

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-opab 4174  df-xp 4757

This theorem is referenced by:  opelxpd  4784  opelvvg  4801  opelvv  4802  opbrop  4831  fnbrfvb2  5721  fliftrel  5967  fnotovb  6098  ovi3  6193  ovres  6196  fovcdm  6199  fnovrn  6204  ovconst2  6208  oprab2co  6416  1stconst  6419  2ndconst  6420  f1od2  6433  brdifun  6796  ecopqsi  6826  brecop  6861  th3q  6876  xpcomco  7079  xpf1o  7099  xpmapenlem  7104  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djuf1olem  7346  cc2lem  7582  addpiord  7633  mulpiord  7634  enqeceq  7676  1nq  7683  addpipqqslem  7686  mulpipq  7689  mulpipqqs  7690  addclnq  7692  mulclnq  7693  recexnq  7707  ltexnqq  7725  prarloclemarch  7735  prarloclemarch2  7736  nnnq  7739  enq0breq  7753  enq0eceq  7754  nqnq0  7758  addnnnq0  7766  mulnnnq0  7767  addclnq0  7768  mulclnq0  7769  nqpnq0nq  7770  prarloclemlt  7810  prarloclemlo  7811  prarloclemcalc  7819  genpelxp  7828  nqprm  7859  ltexprlempr  7925  recexprlempr  7949  cauappcvgprlemcl  7970  cauappcvgprlemladd  7975  caucvgprlemcl  7993  caucvgprprlemcl  8021  enreceq  8053  addsrpr  8062  mulsrpr  8063  0r  8067  1sr  8068  m1r  8069  addclsr  8070  mulclsr  8071  prsrcl  8101  mappsrprg  8121  addcnsr  8151  mulcnsr  8152  addcnsrec  8159  mulcnsrec  8160  pitonnlem2  8164  pitonn  8165  pitore  8167  recnnre  8168  axaddcl  8181  axmulcl  8183  xrlenlt  8340  frecuzrdgg  10782  frecuzrdgsuctlem  10789  seq3val  10826  swrdval  11344  cnrecnv  11599  eucalgf  12756  eucalg  12760  qredeu  12798  qnumdenbi  12893  crth  12925  phimullem  12926  setscom  13269  setsslid  13280  imasaddfnlemg  13544  imasaddflemg  13546  txbas  15140  upxp  15154  uptx  15156  txlm  15161  cnmpt21  15173  txswaphmeolem  15202  txswaphmeo  15203  comet  15381  qtopbasss  15403  cnmetdval  15411  remetdval  15429  tgqioo  15437  dvcnp2cntop  15581  dvef  15609  djucllem  16589  pwle2  16789