Theorem opelxpd 5693

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟨cop 4607   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660

This theorem is referenced by:  otel3xp  5700  opabssxpd  5701  relssdmrn  6257  fpr2g  7203  fliftrel  7301  elovimad  7455  el2xptp0  8035  oprab2co  8096  1stconst  8099  2ndconst  8100  curry2  8106  fsplitfpar  8117  offsplitfpar  8118  fnwelem  8130  xpf1o  9153  xpmapenlem  9158  unxpdomlem3  9260  fseqenlem1  10038  fseqenlem2  10039  iundom2g  10554  ordpipq  10956  addpqf  10958  mulpqf  10960  recmulnq  10978  ltexnq  10989  axmulf  11160  cnrecnv  15184  ruclem1  16249  eucalgf  16602  qredeu  16677  crth  16797  phimullem  16798  prmreclem3  16938  setsstruct2  17193  imasaddflem  17544  xpsaddlem  17587  xpsvsca  17591  xpsle  17593  comffval  17711  oppccofval  17728  isoval  17778  brcic  17811  funcf2  17881  idfu2nd  17890  resf2nd  17908  wunfunc  17914  homaval  18044  setcco  18096  catcco  18118  estrcco  18142  xpcco  18195  xpchom2  18198  xpcco2  18199  xpccatid  18200  prfcl  18215  prf1st  18216  prf2nd  18217  evlf2  18230  curf1cl  18240  curf2cl  18243  curfcl  18244  uncf1  18248  uncf2  18249  uncfcurf  18251  diag11  18255  diag12  18256  diag2  18257  curf2ndf  18259  hof2fval  18267  yonedalem21  18285  yonedalem22  18290  yonedalem3b  18291  yonffthlem  18294  latcl2  18446  xpsmnd0  18756  xpsinv  19043  xpsgrpsub  19044  lsmhash  19686  frgpuplem  19753  xpsring1d  20293  rngqiprngimf  21258  pzriprnglem4  21445  pzriprnglem5  21446  pzriprnglem8  21449  pzriprnglem12  21453  mdetrlin  22540  mdetrsca  22541  txcls  23542  txcnp  23558  txcnmpt  23562  txdis1cn  23573  txlly  23574  txnlly  23575  txlm  23586  lmcn2  23587  txkgen  23590  xkococnlem  23597  txhmeo  23741  ptuncnv  23745  txflf  23944  flfcnp2  23945  tmdcn2  24027  qustgplem  24059  tsmsadd  24085  imasdsf1olem  24312  xpsdsval  24320  comet  24452  metustid  24493  metustexhalf  24495  metuel2  24504  tngnm  24590  cnheiborlem  24904  bcthlem5  25280  ovollb2lem  25441  ovolctb  25443  ovoliunlem2  25456  ovolshftlem1  25462  ovolscalem1  25466  ovolicc1  25469  ioombl1lem1  25511  dyadf  25544  itg1addlem4  25652  limccnp2  25845  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcobr  25901  dvcobrOLD  25902  lhop1lem  25970  cxpcn3  26710  mpodvdsmulf1o  27156  dvdsmulf1o  27158  addsqnreup  27406  addsval  27921  mulsval  28064  tgjustc1  28454  tgjustc2  28455  tgelrnln  28609  numclwwlk1lem2f  30336  ofresid  32620  fsuppcurry1  32702  fsuppcurry2  32703  gsumpart  33051  gsumwrd2dccatlem  33060  gsumwrd2dccat  33061  elrgspnsubrunlem2  33243  erlbrd  33258  rlocaddval  33263  rlocmulval  33264  rloccring  33265  rloc0g  33266  rloc1r  33267  rlocf1  33268  fracerl  33300  fracfld  33302  zringfrac  33569  prsdm  33945  prsrn  33946  esum2dlem  34123  hgt750lemb  34688  cvmlift2lem10  35334  goelel3xp  35370  sat1el2xp  35401  fmla0xp  35405  prv1n  35453  pprodss4v  35902  poimirlem3  37647  poimirlem4  37648  poimirlem17  37661  poimirlem20  37664  mblfinlem2  37682  aks6d1c3  42136  aks6d1c7lem1  42193  f1o2d2  42284  projf1o  45221  ovolval4lem1  46678  ovolval5lem2  46682  gpgiedgdmellem  48050  gpgvtx0  48057  gpgvtx1  48058  gpg3kgrtriex  48091  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem9  48102  tposidres  48861  oppf1st2nd  49079  imaid  49094  xpcfuccocl  49174  swapf1  49189  swapf2val  49190  swapf2  49191  cofuswapf1  49205  cofuswapf2  49206  lanfval  49490  ranfval  49491