Theorem opelxpi 5668

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

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 5667	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 228	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4573   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-xp 5637

This theorem is referenced by:  opelxpii  5669  opelxpd  5670  opelvv  5671  opelvvg  5672  opbrop  5729  elsnxp  6255  reuop  6257  fnbrfvb2  6895  ov3  7530  ovres  7533  fovcdm  7537  fnovrn  7542  ovima0  7546  ovconst2  7547  el2xptp0  7989  opiota  8012  fimaproj  8085  xpord2pred  8095  seqomlem2  8390  brdifun  8674  ecopqsi  8717  brecop  8757  eceqoveq  8769  xpcomco  9005  djulcl  9834  djurcl  9835  djulf1o  9836  djurf1o  9837  djuun  9850  isfin4p1  10237  axdc4lem  10377  canthp1lem2  10576  addpiord  10807  mulpiord  10808  pinq  10850  nqereu  10852  addpipq  10860  addpqnq  10861  mulpipq  10863  mulpqnq  10864  ordpipq  10865  recmulnq  10887  dmrecnq  10891  enreceq  10989  addsrpr  10998  mulsrpr  10999  0r  11003  1sr  11004  m1r  11005  addclsr  11006  mulclsr  11007  axaddf  11068  xrlenlt  11210  uzrdgfni  13920  swrdval  14606  ruclem6  16202  eucalgf  16552  eucalg  16556  qnumdenbi  16714  setscom  17150  strfv2d  17171  setsid  17177  imasaddfnlem  17492  imasaddflem  17494  imasvscafn  17501  imasvscaval  17502  funcpropd  17869  fucco  17932  catcxpccl  18173  curf1cl  18194  curf2cl  18197  curfcl  18198  uncfcurf  18205  diag2  18211  curf2ndf  18213  joindmss  18343  meetdmss  18357  latlem  18403  latjcom  18413  latmcom  18429  efgmf  19688  efglem  19691  vrgpf  19743  vrgpinv  19744  frgpuplem  19747  frgpup2  19751  frgpnabllem1  19848  gsumxp2  19955  rhmsubclem2  20663  pzriprnglem10  21470  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  matsubgcell  22399  matvscacell  22401  pmatcoe1fsupp  22666  txbas  23532  txcls  23569  upxp  23588  uptx  23590  txtube  23605  txcmplem1  23606  txlm  23613  tx1stc  23615  txkgen  23617  cnmpt21  23636  txswaphmeolem  23769  txswaphmeo  23770  clssubg  24074  qustgplem  24086  comet  24478  txmetcnp  24512  metustsym  24520  nrmmetd  24539  isngp3  24563  ngpds  24569  qtopbaslem  24723  cnmetdval  24735  remetdval  24754  tgqioo  24765  bndth  24925  htpyco2  24946  phtpyco2  24957  ovolicc1  25483  ioorf  25540  ioorcl  25544  itg1addlem4  25666  dvcnp2  25887  dvef  25947  lhop1lem  25980  taylthlem2  26339  addsqnreup  27406  addsfo  27975  subsfo  28057  noseqrdgfn  28298  brcgr  28969  ex-fpar  30532  imsdval  30757  sspval  30794  opreu2reuALT  32546  2ndimaxp  32719  ofoprabco  32737  f1od2  32792  qtophaus  33980  mbfmco2  34409  eulerpartlemgh  34522  afsval  34815  erdszelem9  35381  cvmlift2lem1  35484  cvmlift2lem9  35493  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmliftphtlem  35499  goel  35529  goelel3xp  35530  sat1el2xp  35561  fmla0xp  35565  prv1n  35613  msubco  35713  msubff1  35738  mvhf  35740  msubvrs  35742  fvtransport  36214  colinearex  36242  bj-idres  37474  icoreunrn  37675  relowlpssretop  37680  curf  37919  finixpnum  37926  poimirlem15  37956  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  heicant  37976  mblfinlem1  37978  mblfinlem2  37979  ftc1anc  38022  opropabco  38045  heiborlem5  38136  dvhelvbasei  41534  dvhopvadd  41539  dvhvaddcl  41541  dvhopvsca  41548  dvhvscacl  41549  dvhgrp  41553  dvhopclN  41559  dvhopaddN  41560  dvhopspN  41561  dib1dim2  41614  diblss  41616  diclspsn  41640  dih1dimatlem  41775  hoicvrrex  46984  ovnsubaddlem1  46998  ovnhoilem1  47029  ovnlecvr2  47038  opnvonmbllem1  47060  ovolval4lem2  47078  fnotaovb  47646  aovmpt4g  47649  rngccoALTV  48747  rhmsubcALTVlem2  48758  ringccoALTV  48781  rrx2plordisom  49199