Theorem opelxpd 5658

Description: Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
opelxpd.1	⊢ (𝜑 → 𝐴 ∈ 𝐶)
opelxpd.2	⊢ (𝜑 → 𝐵 ∈ 𝐷)

Assertion

Ref	Expression
opelxpd	⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpd

Step	Hyp	Ref	Expression
1		opelxpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		opelxpd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
3		opelxpi 5656	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2111  ⟨cop 4581   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-xp 5625

This theorem is referenced by:  otel3xp  5665  opabssxpd  5666  relssdmrn  6222  fpr2g  7151  fliftrel  7248  elovimad  7402  el2xptp0  7974  oprab2co  8033  1stconst  8036  2ndconst  8037  curry2  8043  fsplitfpar  8054  offsplitfpar  8055  fnwelem  8067  xpf1o  9058  xpmapenlem  9063  unxpdomlem3  9148  fseqenlem1  9921  fseqenlem2  9922  iundom2g  10437  ordpipq  10839  addpqf  10841  mulpqf  10843  recmulnq  10861  ltexnq  10872  axmulf  11043  cnrecnv  15078  ruclem1  16146  eucalgf  16500  qredeu  16575  crth  16695  phimullem  16696  prmreclem3  16836  setsstruct2  17091  imasaddflem  17440  xpsaddlem  17483  xpsvsca  17487  xpsle  17489  comffval  17611  oppccofval  17628  isoval  17678  brcic  17711  funcf2  17781  idfu2nd  17790  resf2nd  17808  wunfunc  17814  homaval  17944  setcco  17996  catcco  18018  estrcco  18042  xpcco  18095  xpchom2  18098  xpcco2  18099  xpccatid  18100  prfcl  18115  prf1st  18116  prf2nd  18117  evlf2  18130  curf1cl  18140  curf2cl  18143  curfcl  18144  uncf1  18148  uncf2  18149  uncfcurf  18151  diag11  18155  diag12  18156  diag2  18157  curf2ndf  18159  hof2fval  18167  yonedalem21  18185  yonedalem22  18190  yonedalem3b  18191  yonffthlem  18194  latcl2  18348  xpsmnd0  18692  xpsinv  18979  xpsgrpsub  18980  lsmhash  19623  frgpuplem  19690  xpsring1d  20257  rngqiprngimf  21240  pzriprnglem4  21427  pzriprnglem5  21428  pzriprnglem8  21431  pzriprnglem12  21435  mdetrlin  22523  mdetrsca  22524  txcls  23525  txcnp  23541  txcnmpt  23545  txdis1cn  23556  txlly  23557  txnlly  23558  txlm  23569  lmcn2  23570  txkgen  23573  xkococnlem  23580  txhmeo  23724  ptuncnv  23728  txflf  23927  flfcnp2  23928  tmdcn2  24010  qustgplem  24042  tsmsadd  24068  imasdsf1olem  24294  xpsdsval  24302  comet  24434  metustid  24475  metustexhalf  24477  metuel2  24486  tngnm  24572  cnheiborlem  24886  bcthlem5  25261  ovollb2lem  25422  ovolctb  25424  ovoliunlem2  25437  ovolshftlem1  25443  ovolscalem1  25447  ovolicc1  25450  ioombl1lem1  25492  dyadf  25525  itg1addlem4  25633  limccnp2  25826  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  lhop1lem  25951  cxpcn3  26691  mpodvdsmulf1o  27137  dvdsmulf1o  27139  addsqnreup  27387  addsval  27911  mulsval  28054  tgjustc1  28459  tgjustc2  28460  tgelrnln  28614  numclwwlk1lem2f  30342  ofresid  32631  fsuppcurry1  32714  fsuppcurry2  32715  gsumpart  33044  gsumwrd2dccatlem  33053  gsumwrd2dccat  33054  elrgspnsubrunlem2  33222  erlbrd  33237  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rloc0g  33245  rloc1r  33246  rlocf1  33247  fracerl  33279  fracfld  33281  zringfrac  33526  prsdm  33934  prsrn  33935  esum2dlem  34112  hgt750lemb  34676  cvmlift2lem10  35363  goelel3xp  35399  sat1el2xp  35430  fmla0xp  35434  prv1n  35482  pprodss4v  35933  poimirlem3  37669  poimirlem4  37670  poimirlem17  37683  poimirlem20  37686  mblfinlem2  37704  aks6d1c3  42222  aks6d1c7lem1  42279  f1o2d2  42332  projf1o  45299  ovolval4lem1  46752  ovolval5lem2  46756  gpgiedgdmellem  48151  gpgvtx0  48158  gpgvtx1  48159  gpg3kgrtriex  48194  gpgprismgr4cycllem3  48202  gpgprismgr4cycllem9  48208  tposidres  48991  oppf1st2nd  49237  imaid  49260  xpcfuccocl  49363  swapf1  49378  swapf2val  49379  swapf2  49380  cofuswapf1  49400  cofuswapf2  49401  lanfval  49719  ranfval  49720