Theorem opelxpi 4529

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 4527	. 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 1461   <.cop 3494   X. cxp 4495

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-opab 3948  df-xp 4503

This theorem is referenced by:  opelxpd  4530  opelvvg  4546  opelvv  4547  opbrop  4576  fliftrel  5645  fnotovb  5766  ovi3  5859  ovres  5862  fovrn  5865  fnovrn  5870  ovconst2  5874  oprab2co  6067  1stconst  6070  2ndconst  6071  f1od2  6084  brdifun  6408  ecopqsi  6436  brecop  6471  th3q  6486  xpcomco  6671  xpf1o  6689  xpmapenlem  6694  djulclr  6884  djurclr  6885  djulcl  6886  djurcl  6887  djuf1olem  6888  addpiord  7066  mulpiord  7067  enqeceq  7109  1nq  7116  addpipqqslem  7119  mulpipq  7122  mulpipqqs  7123  addclnq  7125  mulclnq  7126  recexnq  7140  ltexnqq  7158  prarloclemarch  7168  prarloclemarch2  7169  nnnq  7172  enq0breq  7186  enq0eceq  7187  nqnq0  7191  addnnnq0  7199  mulnnnq0  7200  addclnq0  7201  mulclnq0  7202  nqpnq0nq  7203  prarloclemlt  7243  prarloclemlo  7244  prarloclemcalc  7252  genpelxp  7261  nqprm  7292  ltexprlempr  7358  recexprlempr  7382  cauappcvgprlemcl  7403  cauappcvgprlemladd  7408  caucvgprlemcl  7426  caucvgprprlemcl  7454  enreceq  7473  addsrpr  7482  mulsrpr  7483  0r  7487  1sr  7488  m1r  7489  addclsr  7490  mulclsr  7491  prsrcl  7520  addcnsr  7563  mulcnsr  7564  addcnsrec  7571  mulcnsrec  7572  pitonnlem2  7576  pitonn  7577  pitore  7579  recnnre  7580  axaddcl  7593  axmulcl  7595  xrlenlt  7747  frecuzrdgg  10076  frecuzrdgsuctlem  10083  seq3val  10118  cnrecnv  10569  eucalgf  11576  eucalg  11580  qredeu  11618  qnumdenbi  11709  crth  11739  phimullem  11740  setscom  11836  setsslid  11846  txbas  12263  upxp  12277  uptx  12279  txlm  12284  cnmpt21  12296  comet  12482  qtopbasss  12504  cnmetdval  12512  remetdval  12519  tgqioo  12527  dvcnp2cntop  12612  djucllem  12690  pwle2  12876