Theorem opelxpi 5617

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ⟨cop 4564   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586

This theorem is referenced by:  opelxpd  5618  opelvv  5619  opelvvg  5620  opbrop  5674  elsnxp  6183  reuop  6185  fnbrfvb2  6808  ov3  7413  ovres  7416  fovrn  7420  fnovrn  7425  ovima0  7429  ovconst2  7430  el2xptp0  7851  opiota  7872  fimaproj  7947  seqomlem2  8252  brdifun  8485  ecopqsi  8521  brecop  8557  eceqoveq  8569  xpcomco  8802  djulcl  9599  djurcl  9600  djulf1o  9601  djurf1o  9602  djuun  9615  isfin4p1  10002  axdc4lem  10142  canthp1lem2  10340  addpiord  10571  mulpiord  10572  pinq  10614  nqereu  10616  addpipq  10624  addpqnq  10625  mulpipq  10627  mulpqnq  10628  ordpipq  10629  recmulnq  10651  dmrecnq  10655  enreceq  10753  addsrpr  10762  mulsrpr  10763  0r  10767  1sr  10768  m1r  10769  addclsr  10770  mulclsr  10771  axaddf  10832  xrlenlt  10971  uzrdgfni  13606  swrdval  14284  ruclem6  15872  eucalgf  16216  eucalg  16220  qnumdenbi  16376  setscom  16809  strfv2d  16831  setsid  16837  imasaddfnlem  17156  imasaddflem  17158  imasvscafn  17165  imasvscaval  17166  funcpropd  17532  fucco  17596  catcxpccl  17840  catcxpcclOLD  17841  curf1cl  17862  curf2cl  17865  curfcl  17866  uncfcurf  17873  diag2  17879  curf2ndf  17881  joindmss  18012  meetdmss  18026  latlem  18070  latjcom  18080  latmcom  18096  efgmf  19234  efglem  19237  vrgpf  19289  vrgpinv  19290  frgpuplem  19293  frgpup2  19297  frgpnabllem1  19389  gsumxp2  19496  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  matsubgcell  21491  matvscacell  21493  pmatcoe1fsupp  21758  txbas  22626  txcls  22663  upxp  22682  uptx  22684  txtube  22699  txcmplem1  22700  txlm  22707  tx1stc  22709  txkgen  22711  cnmpt21  22730  txswaphmeolem  22863  txswaphmeo  22864  clssubg  23168  qustgplem  23180  comet  23575  txmetcnp  23609  metustsym  23617  nrmmetd  23636  isngp3  23660  ngpds  23666  qtopbaslem  23828  cnmetdval  23840  remetdval  23858  tgqioo  23869  bndth  24027  htpyco2  24048  phtpyco2  24059  ovolicc1  24585  ioorf  24642  ioorcl  24646  itg1addlem4  24768  itg1addlem4OLD  24769  dvcnp2  24989  dvef  25049  lhop1lem  25082  taylthlem2  25438  addsqnreup  26496  brcgr  27171  ex-fpar  28727  imsdval  28949  sspval  28986  opreu2reuALT  30726  2ndimaxp  30885  ofoprabco  30903  f1od2  30958  qtophaus  31688  mbfmco2  32132  eulerpartlemgh  32245  afsval  32551  erdszelem9  33061  cvmlift2lem1  33164  cvmlift2lem9  33173  cvmlift2lem12  33176  cvmlift2lem13  33177  cvmliftphtlem  33179  goel  33209  goelel3xp  33210  sat1el2xp  33241  fmla0xp  33245  prv1n  33293  msubco  33393  msubff1  33418  mvhf  33420  msubvrs  33422  xpord2pred  33719  fvtransport  34261  colinearex  34289  bj-idres  35258  icoreunrn  35457  relowlpssretop  35462  curf  35682  finixpnum  35689  poimirlem15  35719  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  ftc1anc  35785  opropabco  35809  heiborlem5  35900  dvhelvbasei  39029  dvhopvadd  39034  dvhvaddcl  39036  dvhopvsca  39043  dvhvscacl  39044  dvhgrp  39048  dvhopclN  39054  dvhopaddN  39055  dvhopspN  39056  dib1dim2  39109  diblss  39111  diclspsn  39135  dih1dimatlem  39270  opelxpii  40132  hoicvr  43976  hoicvrrex  43984  ovnsubaddlem1  43998  ovnhoilem1  44029  ovnlecvr2  44038  opnvonmbllem1  44060  ovolval4lem2  44078  fnotaovb  44577  aovmpt4g  44580  rngccoALTV  45434  ringccoALTV  45497  rhmsubclem2  45533  rhmsubcALTVlem2  45551  rrx2plordisom  45957