Theorem opelxpi 4617

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 4615	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2	1	biimpri 132	1 |- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2128   <.cop 3563   X. cxp 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026  df-xp 4591

This theorem is referenced by:  opelxpd  4618  opelvvg  4634  opelvv  4635  opbrop  4664  fliftrel  5739  fnotovb  5861  ovi3  5954  ovres  5957  fovrn  5960  fnovrn  5965  ovconst2  5969  oprab2co  6162  1stconst  6165  2ndconst  6166  f1od2  6179  brdifun  6504  ecopqsi  6532  brecop  6567  th3q  6582  xpcomco  6768  xpf1o  6786  xpmapenlem  6791  djulclr  6987  djurclr  6988  djulcl  6989  djurcl  6990  djuf1olem  6991  cc2lem  7180  addpiord  7230  mulpiord  7231  enqeceq  7273  1nq  7280  addpipqqslem  7283  mulpipq  7286  mulpipqqs  7287  addclnq  7289  mulclnq  7290  recexnq  7304  ltexnqq  7322  prarloclemarch  7332  prarloclemarch2  7333  nnnq  7336  enq0breq  7350  enq0eceq  7351  nqnq0  7355  addnnnq0  7363  mulnnnq0  7364  addclnq0  7365  mulclnq0  7366  nqpnq0nq  7367  prarloclemlt  7407  prarloclemlo  7408  prarloclemcalc  7416  genpelxp  7425  nqprm  7456  ltexprlempr  7522  recexprlempr  7546  cauappcvgprlemcl  7567  cauappcvgprlemladd  7572  caucvgprlemcl  7590  caucvgprprlemcl  7618  enreceq  7650  addsrpr  7659  mulsrpr  7660  0r  7664  1sr  7665  m1r  7666  addclsr  7667  mulclsr  7668  prsrcl  7698  mappsrprg  7718  addcnsr  7748  mulcnsr  7749  addcnsrec  7756  mulcnsrec  7757  pitonnlem2  7761  pitonn  7762  pitore  7764  recnnre  7765  axaddcl  7778  axmulcl  7780  xrlenlt  7936  frecuzrdgg  10308  frecuzrdgsuctlem  10315  seq3val  10350  cnrecnv  10803  eucalgf  11923  eucalg  11927  qredeu  11965  qnumdenbi  12057  crth  12087  phimullem  12088  setscom  12201  setsslid  12211  txbas  12629  upxp  12643  uptx  12645  txlm  12650  cnmpt21  12662  txswaphmeolem  12691  txswaphmeo  12692  comet  12870  qtopbasss  12892  cnmetdval  12900  remetdval  12910  tgqioo  12918  dvcnp2cntop  13034  dvef  13059  djucllem  13345  pwle2  13541