Theorem opelxpi 5661

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 5660	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 228	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ⟨cop 4586   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-xp 5630

This theorem is referenced by:  opelxpii  5662  opelxpd  5663  opelvv  5664  opelvvg  5665  opbrop  5722  elsnxp  6249  reuop  6251  fnbrfvb2  6889  ov3  7521  ovres  7524  fovcdm  7528  fnovrn  7533  ovima0  7537  ovconst2  7538  el2xptp0  7980  opiota  8003  fimaproj  8077  xpord2pred  8087  seqomlem2  8382  brdifun  8665  ecopqsi  8708  brecop  8747  eceqoveq  8759  xpcomco  8995  djulcl  9822  djurcl  9823  djulf1o  9824  djurf1o  9825  djuun  9838  isfin4p1  10225  axdc4lem  10365  canthp1lem2  10564  addpiord  10795  mulpiord  10796  pinq  10838  nqereu  10840  addpipq  10848  addpqnq  10849  mulpipq  10851  mulpqnq  10852  ordpipq  10853  recmulnq  10875  dmrecnq  10879  enreceq  10977  addsrpr  10986  mulsrpr  10987  0r  10991  1sr  10992  m1r  10993  addclsr  10994  mulclsr  10995  axaddf  11056  xrlenlt  11197  uzrdgfni  13881  swrdval  14567  ruclem6  16160  eucalgf  16510  eucalg  16514  qnumdenbi  16671  setscom  17107  strfv2d  17128  setsid  17134  imasaddfnlem  17449  imasaddflem  17451  imasvscafn  17458  imasvscaval  17459  funcpropd  17826  fucco  17889  catcxpccl  18130  curf1cl  18151  curf2cl  18154  curfcl  18155  uncfcurf  18162  diag2  18168  curf2ndf  18170  joindmss  18300  meetdmss  18314  latlem  18360  latjcom  18370  latmcom  18386  efgmf  19642  efglem  19645  vrgpf  19697  vrgpinv  19698  frgpuplem  19701  frgpup2  19705  frgpnabllem1  19802  gsumxp2  19909  rhmsubclem2  20619  pzriprnglem10  21445  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  matsubgcell  22378  matvscacell  22380  pmatcoe1fsupp  22645  txbas  23511  txcls  23548  upxp  23567  uptx  23569  txtube  23584  txcmplem1  23585  txlm  23592  tx1stc  23594  txkgen  23596  cnmpt21  23615  txswaphmeolem  23748  txswaphmeo  23749  clssubg  24053  qustgplem  24065  comet  24457  txmetcnp  24491  metustsym  24499  nrmmetd  24518  isngp3  24542  ngpds  24548  qtopbaslem  24702  cnmetdval  24714  remetdval  24733  tgqioo  24744  bndth  24913  htpyco2  24934  phtpyco2  24945  ovolicc1  25473  ioorf  25530  ioorcl  25534  itg1addlem4  25656  dvcnp2  25877  dvcnp2OLD  25878  dvef  25940  lhop1lem  25974  taylthlem2  26338  taylthlem2OLD  26339  addsqnreup  27410  addsfo  27979  subsfo  28061  noseqrdgfn  28302  brcgr  28973  ex-fpar  30537  imsdval  30761  sspval  30798  opreu2reuALT  32551  2ndimaxp  32724  ofoprabco  32742  f1od2  32798  qtophaus  33993  mbfmco2  34422  eulerpartlemgh  34535  afsval  34828  erdszelem9  35393  cvmlift2lem1  35496  cvmlift2lem9  35505  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmliftphtlem  35511  goel  35541  goelel3xp  35542  sat1el2xp  35573  fmla0xp  35577  prv1n  35625  msubco  35725  msubff1  35750  mvhf  35752  msubvrs  35754  fvtransport  36226  colinearex  36254  bj-idres  37365  icoreunrn  37564  relowlpssretop  37569  curf  37799  finixpnum  37806  poimirlem15  37836  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  heicant  37856  mblfinlem1  37858  mblfinlem2  37859  ftc1anc  37902  opropabco  37925  heiborlem5  38016  dvhelvbasei  41348  dvhopvadd  41353  dvhvaddcl  41355  dvhopvsca  41362  dvhvscacl  41363  dvhgrp  41367  dvhopclN  41373  dvhopaddN  41374  dvhopspN  41375  dib1dim2  41428  diblss  41430  diclspsn  41454  dih1dimatlem  41589  hoicvr  46792  hoicvrrex  46800  ovnsubaddlem1  46814  ovnhoilem1  46845  ovnlecvr2  46854  opnvonmbllem1  46876  ovolval4lem2  46894  fnotaovb  47444  aovmpt4g  47447  rngccoALTV  48517  rhmsubcALTVlem2  48528  ringccoALTV  48551  rrx2plordisom  48969