Theorem opelxpi 5662

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4587   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-xp 5631

This theorem is referenced by:  opelxpii  5663  opelxpd  5664  opelvv  5665  opelvvg  5666  opbrop  5723  elsnxp  6250  reuop  6252  fnbrfvb2  6890  ov3  7523  ovres  7526  fovcdm  7530  fnovrn  7535  ovima0  7539  ovconst2  7540  el2xptp0  7982  opiota  8005  fimaproj  8079  xpord2pred  8089  seqomlem2  8384  brdifun  8668  ecopqsi  8711  brecop  8751  eceqoveq  8763  xpcomco  8999  djulcl  9826  djurcl  9827  djulf1o  9828  djurf1o  9829  djuun  9842  isfin4p1  10229  axdc4lem  10369  canthp1lem2  10568  addpiord  10799  mulpiord  10800  pinq  10842  nqereu  10844  addpipq  10852  addpqnq  10853  mulpipq  10855  mulpqnq  10856  ordpipq  10857  recmulnq  10879  dmrecnq  10883  enreceq  10981  addsrpr  10990  mulsrpr  10991  0r  10995  1sr  10996  m1r  10997  addclsr  10998  mulclsr  10999  axaddf  11060  xrlenlt  11201  uzrdgfni  13885  swrdval  14571  ruclem6  16164  eucalgf  16514  eucalg  16518  qnumdenbi  16675  setscom  17111  strfv2d  17132  setsid  17138  imasaddfnlem  17453  imasaddflem  17455  imasvscafn  17462  imasvscaval  17463  funcpropd  17830  fucco  17893  catcxpccl  18134  curf1cl  18155  curf2cl  18158  curfcl  18159  uncfcurf  18166  diag2  18172  curf2ndf  18174  joindmss  18304  meetdmss  18318  latlem  18364  latjcom  18374  latmcom  18390  efgmf  19646  efglem  19649  vrgpf  19701  vrgpinv  19702  frgpuplem  19705  frgpup2  19709  frgpnabllem1  19806  gsumxp2  19913  rhmsubclem2  20623  pzriprnglem10  21449  mamudi  22351  mamudir  22352  mamuvs1  22353  mamuvs2  22354  matsubgcell  22382  matvscacell  22384  pmatcoe1fsupp  22649  txbas  23515  txcls  23552  upxp  23571  uptx  23573  txtube  23588  txcmplem1  23589  txlm  23596  tx1stc  23598  txkgen  23600  cnmpt21  23619  txswaphmeolem  23752  txswaphmeo  23753  clssubg  24057  qustgplem  24069  comet  24461  txmetcnp  24495  metustsym  24503  nrmmetd  24522  isngp3  24546  ngpds  24552  qtopbaslem  24706  cnmetdval  24718  remetdval  24737  tgqioo  24748  bndth  24917  htpyco2  24938  phtpyco2  24949  ovolicc1  25477  ioorf  25534  ioorcl  25538  itg1addlem4  25660  dvcnp2  25881  dvcnp2OLD  25882  dvef  25944  lhop1lem  25978  taylthlem2  26342  taylthlem2OLD  26343  addsqnreup  27414  addsfo  27983  subsfo  28065  noseqrdgfn  28306  brcgr  28977  ex-fpar  30541  imsdval  30765  sspval  30802  opreu2reuALT  32554  2ndimaxp  32727  ofoprabco  32745  f1od2  32800  qtophaus  33995  mbfmco2  34424  eulerpartlemgh  34537  afsval  34830  erdszelem9  35395  cvmlift2lem1  35498  cvmlift2lem9  35507  cvmlift2lem12  35510  cvmlift2lem13  35511  cvmliftphtlem  35513  goel  35543  goelel3xp  35544  sat1el2xp  35575  fmla0xp  35579  prv1n  35627  msubco  35727  msubff1  35752  mvhf  35754  msubvrs  35756  fvtransport  36228  colinearex  36256  bj-idres  37367  icoreunrn  37566  relowlpssretop  37571  curf  37801  finixpnum  37808  poimirlem15  37838  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  heicant  37858  mblfinlem1  37860  mblfinlem2  37861  ftc1anc  37904  opropabco  37927  heiborlem5  38018  dvhelvbasei  41416  dvhopvadd  41421  dvhvaddcl  41423  dvhopvsca  41430  dvhvscacl  41431  dvhgrp  41435  dvhopclN  41441  dvhopaddN  41442  dvhopspN  41443  dib1dim2  41496  diblss  41498  diclspsn  41522  dih1dimatlem  41657  hoicvr  46859  hoicvrrex  46867  ovnsubaddlem1  46881  ovnhoilem1  46912  ovnlecvr2  46921  opnvonmbllem1  46943  ovolval4lem2  46961  fnotaovb  47511  aovmpt4g  47514  rngccoALTV  48584  rhmsubcALTVlem2  48595  ringccoALTV  48618  rrx2plordisom  49036