Theorem opelxpd 5653

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

Syntax hints:   → wi 4   ∈ wcel 2111  ⟨cop 4579   × cxp 5612

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 5232  ax-nul 5242  ax-pr 5368

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 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5152  df-xp 5620

This theorem is referenced by:  otel3xp  5660  opabssxpd  5661  relssdmrn  6216  fpr2g  7145  fliftrel  7242  elovimad  7396  el2xptp0  7968  oprab2co  8027  1stconst  8030  2ndconst  8031  curry2  8037  fsplitfpar  8048  offsplitfpar  8049  fnwelem  8061  xpf1o  9052  xpmapenlem  9057  unxpdomlem3  9142  fseqenlem1  9915  fseqenlem2  9916  iundom2g  10431  ordpipq  10833  addpqf  10835  mulpqf  10837  recmulnq  10855  ltexnq  10866  axmulf  11037  cnrecnv  15072  ruclem1  16140  eucalgf  16494  qredeu  16569  crth  16689  phimullem  16690  prmreclem3  16830  setsstruct2  17085  imasaddflem  17434  xpsaddlem  17477  xpsvsca  17481  xpsle  17483  comffval  17605  oppccofval  17622  isoval  17672  brcic  17705  funcf2  17775  idfu2nd  17784  resf2nd  17802  wunfunc  17808  homaval  17938  setcco  17990  catcco  18012  estrcco  18036  xpcco  18089  xpchom2  18092  xpcco2  18093  xpccatid  18094  prfcl  18109  prf1st  18110  prf2nd  18111  evlf2  18124  curf1cl  18134  curf2cl  18137  curfcl  18138  uncf1  18142  uncf2  18143  uncfcurf  18145  diag11  18149  diag12  18150  diag2  18151  curf2ndf  18153  hof2fval  18161  yonedalem21  18179  yonedalem22  18184  yonedalem3b  18185  yonffthlem  18188  latcl2  18342  xpsmnd0  18686  xpsinv  18973  xpsgrpsub  18974  lsmhash  19617  frgpuplem  19684  xpsring1d  20251  rngqiprngimf  21234  pzriprnglem4  21421  pzriprnglem5  21422  pzriprnglem8  21425  pzriprnglem12  21429  mdetrlin  22517  mdetrsca  22518  txcls  23519  txcnp  23535  txcnmpt  23539  txdis1cn  23550  txlly  23551  txnlly  23552  txlm  23563  lmcn2  23564  txkgen  23567  xkococnlem  23574  txhmeo  23718  ptuncnv  23722  txflf  23921  flfcnp2  23922  tmdcn2  24004  qustgplem  24036  tsmsadd  24062  imasdsf1olem  24288  xpsdsval  24296  comet  24428  metustid  24469  metustexhalf  24471  metuel2  24480  tngnm  24566  cnheiborlem  24880  bcthlem5  25255  ovollb2lem  25416  ovolctb  25418  ovoliunlem2  25431  ovolshftlem1  25437  ovolscalem1  25441  ovolicc1  25444  ioombl1lem1  25486  dyadf  25519  itg1addlem4  25627  limccnp2  25820  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcobr  25876  dvcobrOLD  25877  lhop1lem  25945  cxpcn3  26685  mpodvdsmulf1o  27131  dvdsmulf1o  27133  addsqnreup  27381  addsval  27905  mulsval  28048  tgjustc1  28453  tgjustc2  28454  tgelrnln  28608  numclwwlk1lem2f  30335  ofresid  32624  fsuppcurry1  32707  fsuppcurry2  32708  gsumpart  33037  gsumwrd2dccatlem  33046  gsumwrd2dccat  33047  elrgspnsubrunlem2  33215  erlbrd  33230  rlocaddval  33235  rlocmulval  33236  rloccring  33237  rloc0g  33238  rloc1r  33239  rlocf1  33240  fracerl  33272  fracfld  33274  zringfrac  33519  prsdm  33927  prsrn  33928  esum2dlem  34105  hgt750lemb  34669  cvmlift2lem10  35356  goelel3xp  35392  sat1el2xp  35423  fmla0xp  35427  prv1n  35475  pprodss4v  35926  poimirlem3  37662  poimirlem4  37663  poimirlem17  37676  poimirlem20  37679  mblfinlem2  37697  aks6d1c3  42215  aks6d1c7lem1  42272  f1o2d2  42325  projf1o  45293  ovolval4lem1  46746  ovolval5lem2  46750  gpgiedgdmellem  48145  gpgvtx0  48152  gpgvtx1  48153  gpg3kgrtriex  48188  gpgprismgr4cycllem3  48196  gpgprismgr4cycllem9  48202  tposidres  48985  oppf1st2nd  49231  imaid  49254  xpcfuccocl  49357  swapf1  49372  swapf2val  49373  swapf2  49374  cofuswapf1  49394  cofuswapf2  49395  lanfval  49713  ranfval  49714