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 2147  ⟨cop 4838   × 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-xp 5661

This theorem is used by:  opelxpii  5693  opelxpd  5694  opelvv  5695  opelvvg  5696  opbrop  5754  elsnxp  6309  reuop  6311  fnbrfvb2  6960  ov3  7604  ovres  7607  fovcdm  7612  fnovrn  7617  ovima0  7621  ovconst2  7622  el2xptp0  8068  opiota  8092  f1od2  8132  fimaproj  8176  xpord2pred  8186  seqomlem2  8486  brdifun  8773  ecopqsi  8816  brecop  8856  eceqoveq  8868  curf  8915  xpcomco  9111  djulcl  10015  djurcl  10016  djulf1o  10017  djurf1o  10018  djuun  10031  isfin4p1  10417  axdc4lem  10557  canthp1lem2  10762  addpiord  10993  mulpiord  10994  pinq  11036  nqereu  11038  addpipq  11046  addpqnq  11047  mulpipq  11049  mulpqnq  11050  ordpipq  11051  recmulnq  11073  dmrecnq  11077  enreceq  11175  addsrpr  11184  mulsrpr  11185  0r  11189  1sr  11190  m1r  11191  addclsr  11192  mulclsr  11193  axaddf  11254  xrlenlt  11398  uzrdgfni  14125  swrdval  14816  ruclem6  16429  eucalgf  16784  eucalg  16788  qnumdenbi  16946  setscom  17384  strfv2d  17405  setsid  17411  imasaddfnlem  17726  imasaddflem  17728  imasvscafn  17735  imasvscaval  17736  funcpropd  18103  fucco  18166  catcxpccl  18407  curf1cl  18428  curf2cl  18431  curfcl  18432  uncfcurf  18439  diag2  18445  curf2ndf  18447  joindmss  18577  meetdmss  18591  latlem  18637  latjcom  18647  latmcom  18663  mgmn0plusgplusf  18854  efgmf  19954  efglem  19957  vrgpf  20009  vrgpinv  20010  frgpuplem  20013  frgpup2  20017  frgpnabllem1  20114  gsumxp2  20221  rhmsubclem2  20965  pzriprnglem10  21823  mamudi  22745  mamudir  22746  mamuvs1  22747  mamuvs2  22748  matsubgcell  22776  matvscacell  22778  pmatcoe1fsupp  23046  txbas  23913  txcls  23950  upxp  23969  uptx  23971  txtube  23986  txcmplem1  23987  txlm  23994  tx1stc  23996  txkgen  23998  cnmpt21  24017  txswaphmeolem  24150  txswaphmeo  24151  clssubg  24455  qustgplem  24467  comet  24859  txmetcnp  24893  metustsym  24901  nrmmetd  24920  isngp3  24944  ngpds  24950  qtopbaslem  25104  cnmetdval  25116  remetdval  25135  tgqioo  25146  bndth  25306  htpyco2  25327  phtpyco2  25338  ovolicc1  25864  ioorf  25921  ioorcl  25925  itg1addlem4  26047  dvcnp2  26267  dvef  26327  lhop1lem  26360  taylthlem2  26728  addsqnreup  27797  addsfo  28396  subsfo  28478  noseqrdgfn  28719  brcgr  29505  ex-fpar  31090  imsdval  31315  sspval  31352  opreu2reuALT  33142  2ndimaxp  33309  ofoprabco  33327  qtophaus  34535  mbfmco2  34964  eulerpartlemgh  35077  afsval  35370  j00smo  36004  maxssj0  36005  j0ltalephlem  36006  erdszelem9  36130  cvmlift2lem1  36233  cvmlift2lem9  36242  cvmlift2lem12  36245  cvmlift2lem13  36246  cvmliftphtlem  36248  goel  36278  goelel3xp  36279  sat1el2xp  36310  fmla0xp  36314  prv1n  36362  msubco  36462  msubff1  36487  mvhf  36489  msubvrs  36491  fvtransport  36974  colinearex  37002  nmulprop  37116  bj-idres  38272  icoreunrn  38473  relowlpssretop  38478  finixpnum  38719  poimirlem15  38744  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  heicant  38764  mblfinlem1  38766  mblfinlem2  38767  ftc1anc  38810  opropabco  38849  heiborlem5  38940  dvhelvbasei  42336  dvhopvadd  42341  dvhvaddcl  42343  dvhopvsca  42350  dvhvscacl  42351  dvhgrp  42355  dvhopclN  42361  dvhopaddN  42362  dvhopspN  42363  dib1dim2  42416  diblss  42418  diclspsn  42442  dih1dimatlem  42577  hoicvrrex  47769  ovnsubaddlem1  47783  ovnhoilem1  47814  ovnlecvr2  47823  opnvonmbllem1  47845  ovolval4lem2  47863  fnotaovb  48471  aovmpt4g  48474  rngccoALTV  49571  rhmsubcALTVlem2  49582  ringccoALTV  49605  rrx2plordisom  50039