Theorem opelxpi 4696

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 4694	. 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 2167   <.cop 3626   X. cxp 4662

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-opab 4096  df-xp 4670

This theorem is referenced by:  opelxpd  4697  opelvvg  4713  opelvv  4714  opbrop  4743  fliftrel  5842  fnotovb  5969  ovi3  6064  ovres  6067  fovcdm  6070  fnovrn  6075  ovconst2  6079  oprab2co  6285  1stconst  6288  2ndconst  6289  f1od2  6302  brdifun  6628  ecopqsi  6658  brecop  6693  th3q  6708  xpcomco  6894  xpf1o  6914  xpmapenlem  6919  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuf1olem  7128  cc2lem  7349  addpiord  7400  mulpiord  7401  enqeceq  7443  1nq  7450  addpipqqslem  7453  mulpipq  7456  mulpipqqs  7457  addclnq  7459  mulclnq  7460  recexnq  7474  ltexnqq  7492  prarloclemarch  7502  prarloclemarch2  7503  nnnq  7506  enq0breq  7520  enq0eceq  7521  nqnq0  7525  addnnnq0  7533  mulnnnq0  7534  addclnq0  7535  mulclnq0  7536  nqpnq0nq  7537  prarloclemlt  7577  prarloclemlo  7578  prarloclemcalc  7586  genpelxp  7595  nqprm  7626  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  cauappcvgprlemladd  7742  caucvgprlemcl  7760  caucvgprprlemcl  7788  enreceq  7820  addsrpr  7829  mulsrpr  7830  0r  7834  1sr  7835  m1r  7836  addclsr  7837  mulclsr  7838  prsrcl  7868  mappsrprg  7888  addcnsr  7918  mulcnsr  7919  addcnsrec  7926  mulcnsrec  7927  pitonnlem2  7931  pitonn  7932  pitore  7934  recnnre  7935  axaddcl  7948  axmulcl  7950  xrlenlt  8108  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seq3val  10569  cnrecnv  11092  eucalgf  12248  eucalg  12252  qredeu  12290  qnumdenbi  12385  crth  12417  phimullem  12418  setscom  12743  setsslid  12754  imasaddfnlemg  13016  imasaddflemg  13018  txbas  14578  upxp  14592  uptx  14594  txlm  14599  cnmpt21  14611  txswaphmeolem  14640  txswaphmeo  14641  comet  14819  qtopbasss  14841  cnmetdval  14849  remetdval  14867  tgqioo  14875  dvcnp2cntop  15019  dvef  15047  djucllem  15530  pwle2  15729