Theorem opelxpd 5662

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 5660	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4585   × cxp 5621

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 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

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 2714  df-cleq 2727  df-clel 2810  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5160  df-xp 5629

This theorem is referenced by:  otel3xp  5669  opabssxpd  5670  relssdmrn  6226  fpr2g  7157  fliftrel  7254  elovimad  7408  el2xptp0  7980  oprab2co  8039  1stconst  8042  2ndconst  8043  curry2  8049  fsplitfpar  8060  offsplitfpar  8061  fnwelem  8073  xpf1o  9069  xpmapenlem  9074  unxpdomlem3  9160  fseqenlem1  9936  fseqenlem2  9937  iundom2g  10452  ordpipq  10855  addpqf  10857  mulpqf  10859  recmulnq  10877  ltexnq  10888  axmulf  11059  cnrecnv  15090  ruclem1  16158  eucalgf  16512  qredeu  16587  crth  16707  phimullem  16708  prmreclem3  16848  setsstruct2  17103  imasaddflem  17453  xpsaddlem  17496  xpsvsca  17500  xpsle  17502  comffval  17624  oppccofval  17641  isoval  17691  brcic  17724  funcf2  17794  idfu2nd  17803  resf2nd  17821  wunfunc  17827  homaval  17957  setcco  18009  catcco  18031  estrcco  18055  xpcco  18108  xpchom2  18111  xpcco2  18112  xpccatid  18113  prfcl  18128  prf1st  18129  prf2nd  18130  evlf2  18143  curf1cl  18153  curf2cl  18156  curfcl  18157  uncf1  18161  uncf2  18162  uncfcurf  18164  diag11  18168  diag12  18169  diag2  18170  curf2ndf  18172  hof2fval  18180  yonedalem21  18198  yonedalem22  18203  yonedalem3b  18204  yonffthlem  18207  latcl2  18361  xpsmnd0  18705  xpsinv  18992  xpsgrpsub  18993  lsmhash  19636  frgpuplem  19703  xpsring1d  20271  rngqiprngimf  21254  pzriprnglem4  21441  pzriprnglem5  21442  pzriprnglem8  21445  pzriprnglem12  21449  mdetrlin  22548  mdetrsca  22549  txcls  23550  txcnp  23566  txcnmpt  23570  txdis1cn  23581  txlly  23582  txnlly  23583  txlm  23594  lmcn2  23595  txkgen  23598  xkococnlem  23605  txhmeo  23749  ptuncnv  23753  txflf  23952  flfcnp2  23953  tmdcn2  24035  qustgplem  24067  tsmsadd  24093  imasdsf1olem  24319  xpsdsval  24327  comet  24459  metustid  24500  metustexhalf  24502  metuel2  24511  tngnm  24597  cnheiborlem  24911  bcthlem5  25286  ovollb2lem  25447  ovolctb  25449  ovoliunlem2  25462  ovolshftlem1  25468  ovolscalem1  25472  ovolicc1  25475  ioombl1lem1  25517  dyadf  25550  itg1addlem4  25658  limccnp2  25851  dvaddbr  25898  dvmulbr  25899  dvmulbrOLD  25900  dvcobr  25907  dvcobrOLD  25908  lhop1lem  25976  cxpcn3  26716  mpodvdsmulf1o  27162  dvdsmulf1o  27164  addsqnreup  27412  addsval  27942  mulsval  28089  tgjustc1  28528  tgjustc2  28529  tgelrnln  28683  numclwwlk1lem2f  30411  ofresid  32700  fsuppcurry1  32782  fsuppcurry2  32783  gsumpart  33125  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  elrgspnsubrunlem2  33309  erlbrd  33324  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  fracerl  33367  fracfld  33369  zringfrac  33614  prsdm  34050  prsrn  34051  esum2dlem  34228  hgt750lemb  34792  cvmlift2lem10  35485  goelel3xp  35521  sat1el2xp  35552  fmla0xp  35556  prv1n  35604  pprodss4v  36055  poimirlem3  37793  poimirlem4  37794  poimirlem17  37807  poimirlem20  37810  mblfinlem2  37828  aks6d1c3  42412  aks6d1c7lem1  42469  f1o2d2  42527  projf1o  45478  ovolval4lem1  46930  ovolval5lem2  46934  gpgiedgdmellem  48329  gpgvtx0  48336  gpgvtx1  48337  gpg3kgrtriex  48372  gpgprismgr4cycllem3  48380  gpgprismgr4cycllem9  48386  tposidres  49168  oppf1st2nd  49413  imaid  49436  xpcfuccocl  49539  swapf1  49554  swapf2val  49555  swapf2  49556  cofuswapf1  49576  cofuswapf2  49577  lanfval  49895  ranfval  49896