Theorem opelxpi 5379

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164  ⟨cop 4403   × cxp 5340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-opab 4936  df-xp 5348

This theorem is referenced by:  opelxpd  5380  opelvv  5381  opelvvg  5382  opbrop  5433  elsnxp  5918  fnbrfvb2  6486  fpr2g  6731  fliftrel  6813  elovimad  6952  ov3  7057  ovres  7060  fovrn  7064  fnovrn  7069  ovima0  7073  ovconst2  7074  el2xptp0  7474  opiota  7491  oprab2co  7526  seqomlem2  7812  brdifun  8038  ecopqsi  8069  brecop  8105  eceqoveq  8118  xpcomco  8319  xpf1o  8391  unxpdomlem3  8435  djulcl  9049  djurcl  9050  djulf1o  9051  djurf1o  9052  djuun  9065  fseqenlem1  9160  fseqenlem2  9161  isfin4-3  9452  axdc4lem  9592  iundom2g  9677  canthp1lem2  9790  addpiord  10021  mulpiord  10022  pinq  10064  nqereu  10066  addpipq  10074  addpqnq  10075  mulpipq  10077  mulpqnq  10078  ordpipq  10079  addpqf  10081  mulpqf  10083  recmulnq  10101  dmrecnq  10105  ltexnq  10112  enreceq  10203  addsrpr  10212  mulsrpr  10213  0r  10217  1sr  10218  m1r  10219  addclsr  10220  mulclsr  10221  axaddf  10282  axmulf  10283  xrlenlt  10422  uzrdgfni  13052  swrdval  13703  cnrecnv  14282  ruclem1  15334  ruclem6  15338  eucalgf  15669  eucalg  15673  qnumdenbi  15823  crth  15854  phimullem  15855  prmreclem3  15993  setscom  16266  strfv2d  16268  setsid  16277  imasaddfnlem  16541  imasaddflem  16543  imasvscafn  16550  imasvscaval  16551  xpsaddlem  16588  xpsvsca  16592  xpsle  16594  comffval  16711  oppccofval  16728  isoval  16777  funcf2  16880  idfu2nd  16889  resf2nd  16907  wunfunc  16911  funcpropd  16912  fucco  16974  homaval  17033  setcco  17085  catcco  17103  estrcco  17122  xpcco  17176  xpchom2  17179  xpcco2  17180  xpccatid  17181  prfcl  17196  prf1st  17197  prf2nd  17198  catcxpccl  17200  evlf2  17211  curf1cl  17221  curf2cl  17224  curfcl  17225  uncf1  17229  uncf2  17230  uncfcurf  17232  diag11  17236  diag12  17237  diag2  17238  curf2ndf  17240  hof2fval  17248  yonedalem21  17266  yonedalem22  17271  yonedalem3b  17272  yonffthlem  17275  joindmss  17360  meetdmss  17374  latcl2  17401  latlem  17402  latjcom  17412  latmcom  17428  lsmhash  18469  efgmf  18477  efglem  18480  vrgpf  18534  vrgpinv  18535  frgpuplem  18538  frgpup2  18542  frgpnabllem1  18629  mamudi  20576  mamudir  20577  mamuvs1  20578  mamuvs2  20579  matsubgcell  20607  matvscacell  20609  mdetrsca  20777  pmatcoe1fsupp  20876  txbas  21741  txcls  21778  txcnp  21794  upxp  21797  txcnmpt  21798  uptx  21799  txlly  21810  txnlly  21811  txtube  21814  txcmplem1  21815  txlm  21822  lmcn2  21823  tx1stc  21824  txkgen  21826  xkococnlem  21833  cnmpt21  21845  txhmeo  21977  txswaphmeolem  21978  txswaphmeo  21979  ptuncnv  21981  txflf  22180  flfcnp2  22181  tmdcn2  22263  clssubg  22282  qustgplem  22294  tsmsadd  22320  imasdsf1olem  22548  xpsdsval  22556  comet  22688  txmetcnp  22722  metustsym  22730  nrmmetd  22749  isngp3  22772  ngpds  22778  tngnm  22825  qtopbaslem  22932  cnmetdval  22944  remetdval  22962  tgqioo  22973  bndth  23127  htpyco2  23148  phtpyco2  23159  bcthlem5  23496  ovollb2lem  23654  ovolctb  23656  ovoliunlem2  23669  ovolscalem1  23679  ovolicc1  23682  ioombl1lem1  23724  ioorf  23739  ioorcl  23743  dyadf  23757  itg1addlem4  23865  limccnp2  24055  dvcnp2  24082  dvaddbr  24100  dvmulbr  24101  dvcobr  24108  dvef  24142  lhop1lem  24175  taylthlem2  24527  dvdsmulf1o  25333  tgelrnln  25942  brcgr  26199  imsdval  28085  sspval  28122  ofoprabco  30002  f1od2  30036  fimaproj  30434  qtophaus  30437  prsdm  30494  prsrn  30495  mbfmco2  30861  eulerpartlemgh  30974  afsval  31287  erdszelem9  31716  cvmlift2lem1  31819  cvmlift2lem9  31828  cvmlift2lem12  31831  cvmlift2lem13  31832  cvmliftphtlem  31834  msubco  31963  msubff1  31988  mvhf  31990  msubvrs  31992  fvtransport  32667  colinearex  32695  icoreunrn  33745  relowlpssretop  33750  cnfinltrel  33779  curf  33923  finixpnum  33930  poimirlem3  33949  poimirlem4  33950  poimirlem15  33961  poimirlem17  33963  poimirlem20  33966  poimirlem25  33971  poimirlem26  33972  poimirlem27  33973  heicant  33981  mblfinlem1  33983  mblfinlem2  33984  ftc1anc  34029  opropabco  34054  heiborlem5  34149  dvhelvbasei  37156  dvhopvadd  37161  dvhvaddcl  37163  dvhopvsca  37170  dvhvscacl  37171  dvhgrp  37175  dvhopclN  37181  dvhopaddN  37182  dvhopspN  37183  dib1dim2  37236  diblss  37238  diclspsn  37262  dih1dimatlem  37397  opelxpii  38038  projf1o  40187  hoicvr  41549  hoicvrrex  41557  ovnsubaddlem1  41571  ovnhoilem1  41602  ovnlecvr2  41611  opnvonmbllem1  41633  ovolval4lem2  41651  fnotaovb  42093  aovmpt4g  42096  rngccoALTV  42828  ringccoALTV  42891  rhmsubclem2  42927  rhmsubcALTVlem2  42945