Theorem opelxpi 5692

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ⟨cop 4590   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5661

This theorem is used by:  opelxpii  5693  opelxpd  5694  opelvv  5695  opelvvg  5696  opbrop  5753  elsnxp  6291  reuop  6293  fnbrfvb2  6936  ov3  7579  ovres  7582  fovcdm  7587  fnovrn  7592  ovima0  7596  ovconst2  7597  el2xptp0  8038  opiota  8061  fimaproj  8138  xpord2pred  8148  seqomlem2  8447  brdifun  8734  ecopqsi  8777  brecop  8817  eceqoveq  8829  curf  8876  xpcomco  9072  djulcl  9940  djurcl  9941  djulf1o  9942  djurf1o  9943  djuun  9956  isfin4p1  10342  axdc4lem  10482  canthp1lem2  10687  addpiord  10918  mulpiord  10919  pinq  10961  nqereu  10963  addpipq  10971  addpqnq  10972  mulpipq  10974  mulpqnq  10975  ordpipq  10976  recmulnq  10998  dmrecnq  11002  enreceq  11100  addsrpr  11109  mulsrpr  11110  0r  11114  1sr  11115  m1r  11116  addclsr  11117  mulclsr  11118  axaddf  11179  xrlenlt  11323  uzrdgfni  14047  swrdval  14736  ruclem6  16348  eucalgf  16698  eucalg  16702  qnumdenbi  16860  setscom  17297  strfv2d  17318  setsid  17324  imasaddfnlem  17639  imasaddflem  17641  imasvscafn  17648  imasvscaval  17649  funcpropd  18016  fucco  18079  catcxpccl  18320  curf1cl  18341  curf2cl  18344  curfcl  18345  uncfcurf  18352  diag2  18358  curf2ndf  18360  joindmss  18490  meetdmss  18504  latlem  18550  latjcom  18560  latmcom  18576  mgmn0plusgplusf  18767  efgmf  19866  efglem  19869  vrgpf  19921  vrgpinv  19922  frgpuplem  19925  frgpup2  19929  frgpnabllem1  20026  gsumxp2  20133  rhmsubclem2  20877  pzriprnglem10  21735  mamudi  22657  mamudir  22658  mamuvs1  22659  mamuvs2  22660  matsubgcell  22688  matvscacell  22690  pmatcoe1fsupp  22958  txbas  23825  txcls  23862  upxp  23881  uptx  23883  txtube  23898  txcmplem1  23899  txlm  23906  tx1stc  23908  txkgen  23910  cnmpt21  23929  txswaphmeolem  24062  txswaphmeo  24063  clssubg  24367  qustgplem  24379  comet  24771  txmetcnp  24805  metustsym  24813  nrmmetd  24832  isngp3  24856  ngpds  24862  qtopbaslem  25016  cnmetdval  25028  remetdval  25047  tgqioo  25058  bndth  25218  htpyco2  25239  phtpyco2  25250  ovolicc1  25776  ioorf  25833  ioorcl  25837  itg1addlem4  25959  dvcnp2  26179  dvef  26239  lhop1lem  26272  taylthlem2  26642  addsqnreup  27711  addsfo  28280  subsfo  28362  noseqrdgfn  28603  brcgr  29389  ex-fpar  30974  imsdval  31199  sspval  31236  opreu2reuALT  32984  2ndimaxp  33151  ofoprabco  33169  f1od2  33222  qtophaus  34379  mbfmco2  34809  eulerpartlemgh  34922  afsval  35215  erdszelem9  35861  cvmlift2lem1  35964  cvmlift2lem9  35973  cvmlift2lem12  35976  cvmlift2lem13  35977  cvmliftphtlem  35979  goel  36009  goelel3xp  36010  sat1el2xp  36041  fmla0xp  36045  prv1n  36093  msubco  36193  msubff1  36218  mvhf  36220  msubvrs  36222  fvtransport  36695  colinearex  36723  nmulprop  36837  bj-idres  37977  icoreunrn  38178  relowlpssretop  38183  finixpnum  38424  poimirlem15  38449  poimirlem25  38459  poimirlem26  38460  poimirlem27  38461  heicant  38469  mblfinlem1  38471  mblfinlem2  38472  ftc1anc  38515  opropabco  38539  heiborlem5  38630  dvhelvbasei  42026  dvhopvadd  42031  dvhvaddcl  42033  dvhopvsca  42040  dvhvscacl  42041  dvhgrp  42045  dvhopclN  42051  dvhopaddN  42052  dvhopspN  42053  dib1dim2  42106  diblss  42108  diclspsn  42132  dih1dimatlem  42267  hoicvrrex  47449  ovnsubaddlem1  47463  ovnhoilem1  47494  ovnlecvr2  47503  opnvonmbllem1  47525  ovolval4lem2  47543  fnotaovb  48151  aovmpt4g  48154  rngccoALTV  49251  rhmsubcALTVlem2  49262  ringccoALTV  49285  rrx2plordisom  49718