Theorem opelxpi 5678

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ⟨cop 4598   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-xp 5647

This theorem is referenced by:  opelxpii  5679  opelxpd  5680  opelvv  5681  opelvvg  5682  opbrop  5739  elsnxp  6267  reuop  6269  fnbrfvb2  6919  ov3  7555  ovres  7558  fovcdm  7562  fnovrn  7567  ovima0  7571  ovconst2  7572  el2xptp0  8018  opiota  8041  fimaproj  8117  xpord2pred  8127  seqomlem2  8422  brdifun  8704  ecopqsi  8747  brecop  8786  eceqoveq  8798  xpcomco  9036  djulcl  9870  djurcl  9871  djulf1o  9872  djurf1o  9873  djuun  9886  isfin4p1  10275  axdc4lem  10415  canthp1lem2  10613  addpiord  10844  mulpiord  10845  pinq  10887  nqereu  10889  addpipq  10897  addpqnq  10898  mulpipq  10900  mulpqnq  10901  ordpipq  10902  recmulnq  10924  dmrecnq  10928  enreceq  11026  addsrpr  11035  mulsrpr  11036  0r  11040  1sr  11041  m1r  11042  addclsr  11043  mulclsr  11044  axaddf  11105  xrlenlt  11246  uzrdgfni  13930  swrdval  14615  ruclem6  16210  eucalgf  16560  eucalg  16564  qnumdenbi  16721  setscom  17157  strfv2d  17178  setsid  17184  imasaddfnlem  17498  imasaddflem  17500  imasvscafn  17507  imasvscaval  17508  funcpropd  17871  fucco  17934  catcxpccl  18175  curf1cl  18196  curf2cl  18199  curfcl  18200  uncfcurf  18207  diag2  18213  curf2ndf  18215  joindmss  18345  meetdmss  18359  latlem  18403  latjcom  18413  latmcom  18429  efgmf  19650  efglem  19653  vrgpf  19705  vrgpinv  19706  frgpuplem  19709  frgpup2  19713  frgpnabllem1  19810  gsumxp2  19917  rhmsubclem2  20602  pzriprnglem10  21407  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  matsubgcell  22328  matvscacell  22330  pmatcoe1fsupp  22595  txbas  23461  txcls  23498  upxp  23517  uptx  23519  txtube  23534  txcmplem1  23535  txlm  23542  tx1stc  23544  txkgen  23546  cnmpt21  23565  txswaphmeolem  23698  txswaphmeo  23699  clssubg  24003  qustgplem  24015  comet  24408  txmetcnp  24442  metustsym  24450  nrmmetd  24469  isngp3  24493  ngpds  24499  qtopbaslem  24653  cnmetdval  24665  remetdval  24684  tgqioo  24695  bndth  24864  htpyco2  24885  phtpyco2  24896  ovolicc1  25424  ioorf  25481  ioorcl  25485  itg1addlem4  25607  dvcnp2  25828  dvcnp2OLD  25829  dvef  25891  lhop1lem  25925  taylthlem2  26289  taylthlem2OLD  26290  addsqnreup  27361  addsfo  27897  subsfo  27976  noseqrdgfn  28207  brcgr  28834  ex-fpar  30398  imsdval  30622  sspval  30659  opreu2reuALT  32413  2ndimaxp  32577  ofoprabco  32595  f1od2  32651  qtophaus  33833  mbfmco2  34263  eulerpartlemgh  34376  afsval  34669  erdszelem9  35193  cvmlift2lem1  35296  cvmlift2lem9  35305  cvmlift2lem12  35308  cvmlift2lem13  35309  cvmliftphtlem  35311  goel  35341  goelel3xp  35342  sat1el2xp  35373  fmla0xp  35377  prv1n  35425  msubco  35525  msubff1  35550  mvhf  35552  msubvrs  35554  fvtransport  36027  colinearex  36055  bj-idres  37155  icoreunrn  37354  relowlpssretop  37359  curf  37599  finixpnum  37606  poimirlem15  37636  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  ftc1anc  37702  opropabco  37725  heiborlem5  37816  dvhelvbasei  41089  dvhopvadd  41094  dvhvaddcl  41096  dvhopvsca  41103  dvhvscacl  41104  dvhgrp  41108  dvhopclN  41114  dvhopaddN  41115  dvhopspN  41116  dib1dim2  41169  diblss  41171  diclspsn  41195  dih1dimatlem  41330  hoicvr  46553  hoicvrrex  46561  ovnsubaddlem1  46575  ovnhoilem1  46606  ovnlecvr2  46615  opnvonmbllem1  46637  ovolval4lem2  46655  fnotaovb  47203  aovmpt4g  47206  rngccoALTV  48263  rhmsubcALTVlem2  48274  ringccoALTV  48297  rrx2plordisom  48716