Theorem opelxpi 5737

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-xp 5706

This theorem is referenced by:  opelxpii  5738  opelxpd  5739  opelvv  5740  opelvvg  5741  opbrop  5797  elsnxp  6322  reuop  6324  fnbrfvb2  6977  ov3  7613  ovres  7616  fovcdm  7620  fnovrn  7625  ovima0  7629  ovconst2  7630  el2xptp0  8077  opiota  8100  fimaproj  8176  xpord2pred  8186  seqomlem2  8507  brdifun  8793  ecopqsi  8832  brecop  8868  eceqoveq  8880  xpcomco  9128  djulcl  9979  djurcl  9980  djulf1o  9981  djurf1o  9982  djuun  9995  isfin4p1  10384  axdc4lem  10524  canthp1lem2  10722  addpiord  10953  mulpiord  10954  pinq  10996  nqereu  10998  addpipq  11006  addpqnq  11007  mulpipq  11009  mulpqnq  11010  ordpipq  11011  recmulnq  11033  dmrecnq  11037  enreceq  11135  addsrpr  11144  mulsrpr  11145  0r  11149  1sr  11150  m1r  11151  addclsr  11152  mulclsr  11153  axaddf  11214  xrlenlt  11355  uzrdgfni  14009  swrdval  14691  ruclem6  16283  eucalgf  16630  eucalg  16634  qnumdenbi  16791  setscom  17227  strfv2d  17249  setsid  17255  imasaddfnlem  17588  imasaddflem  17590  imasvscafn  17597  imasvscaval  17598  funcpropd  17967  fucco  18032  catcxpccl  18276  catcxpcclOLD  18277  curf1cl  18298  curf2cl  18301  curfcl  18302  uncfcurf  18309  diag2  18315  curf2ndf  18317  joindmss  18449  meetdmss  18463  latlem  18507  latjcom  18517  latmcom  18533  efgmf  19755  efglem  19758  vrgpf  19810  vrgpinv  19811  frgpuplem  19814  frgpup2  19818  frgpnabllem1  19915  gsumxp2  20022  rhmsubclem2  20708  pzriprnglem10  21524  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  matsubgcell  22461  matvscacell  22463  pmatcoe1fsupp  22728  txbas  23596  txcls  23633  upxp  23652  uptx  23654  txtube  23669  txcmplem1  23670  txlm  23677  tx1stc  23679  txkgen  23681  cnmpt21  23700  txswaphmeolem  23833  txswaphmeo  23834  clssubg  24138  qustgplem  24150  comet  24547  txmetcnp  24581  metustsym  24589  nrmmetd  24608  isngp3  24632  ngpds  24638  qtopbaslem  24800  cnmetdval  24812  remetdval  24830  tgqioo  24841  bndth  25009  htpyco2  25030  phtpyco2  25041  ovolicc1  25570  ioorf  25627  ioorcl  25631  itg1addlem4  25753  itg1addlem4OLD  25754  dvcnp2  25975  dvcnp2OLD  25976  dvef  26038  lhop1lem  26072  taylthlem2  26434  taylthlem2OLD  26435  addsqnreup  27505  addsfo  28034  subsfo  28113  noseqrdgfn  28330  brcgr  28933  ex-fpar  30494  imsdval  30718  sspval  30755  opreu2reuALT  32505  2ndimaxp  32665  ofoprabco  32682  f1od2  32735  qtophaus  33782  mbfmco2  34230  eulerpartlemgh  34343  afsval  34648  erdszelem9  35167  cvmlift2lem1  35270  cvmlift2lem9  35279  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmliftphtlem  35285  goel  35315  goelel3xp  35316  sat1el2xp  35347  fmla0xp  35351  prv1n  35399  msubco  35499  msubff1  35524  mvhf  35526  msubvrs  35528  fvtransport  35996  colinearex  36024  bj-idres  37126  icoreunrn  37325  relowlpssretop  37330  curf  37558  finixpnum  37565  poimirlem15  37595  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  heicant  37615  mblfinlem1  37617  mblfinlem2  37618  ftc1anc  37661  opropabco  37684  heiborlem5  37775  dvhelvbasei  41045  dvhopvadd  41050  dvhvaddcl  41052  dvhopvsca  41059  dvhvscacl  41060  dvhgrp  41064  dvhopclN  41070  dvhopaddN  41071  dvhopspN  41072  dib1dim2  41125  diblss  41127  diclspsn  41151  dih1dimatlem  41286  hoicvr  46469  hoicvrrex  46477  ovnsubaddlem1  46491  ovnhoilem1  46522  ovnlecvr2  46531  opnvonmbllem1  46553  ovolval4lem2  46571  fnotaovb  47113  aovmpt4g  47116  rngccoALTV  47994  rhmsubcALTVlem2  48005  ringccoALTV  48028  rrx2plordisom  48457