Theorem opelxpd 5670

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

Syntax hints:   → wi 4   ∈ wcel 2109  ⟨cop 4591   × cxp 5629

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637

This theorem is referenced by:  otel3xp  5677  opabssxpd  5678  relssdmrn  6229  fpr2g  7167  fliftrel  7265  elovimad  7419  el2xptp0  7994  oprab2co  8053  1stconst  8056  2ndconst  8057  curry2  8063  fsplitfpar  8074  offsplitfpar  8075  fnwelem  8087  xpf1o  9080  xpmapenlem  9085  unxpdomlem3  9175  fseqenlem1  9955  fseqenlem2  9956  iundom2g  10471  ordpipq  10873  addpqf  10875  mulpqf  10877  recmulnq  10895  ltexnq  10906  axmulf  11077  cnrecnv  15108  ruclem1  16176  eucalgf  16530  qredeu  16605  crth  16725  phimullem  16726  prmreclem3  16866  setsstruct2  17121  imasaddflem  17470  xpsaddlem  17513  xpsvsca  17517  xpsle  17519  comffval  17641  oppccofval  17658  isoval  17708  brcic  17741  funcf2  17811  idfu2nd  17820  resf2nd  17838  wunfunc  17844  homaval  17974  setcco  18026  catcco  18048  estrcco  18072  xpcco  18125  xpchom2  18128  xpcco2  18129  xpccatid  18130  prfcl  18145  prf1st  18146  prf2nd  18147  evlf2  18160  curf1cl  18170  curf2cl  18173  curfcl  18174  uncf1  18178  uncf2  18179  uncfcurf  18181  diag11  18185  diag12  18186  diag2  18187  curf2ndf  18189  hof2fval  18197  yonedalem21  18215  yonedalem22  18220  yonedalem3b  18221  yonffthlem  18224  latcl2  18378  xpsmnd0  18688  xpsinv  18975  xpsgrpsub  18976  lsmhash  19620  frgpuplem  19687  xpsring1d  20254  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  24295  xpsdsval  24303  comet  24435  metustid  24476  metustexhalf  24478  metuel2  24487  tngnm  24573  cnheiborlem  24887  bcthlem5  25262  ovollb2lem  25423  ovolctb  25425  ovoliunlem2  25438  ovolshftlem1  25444  ovolscalem1  25448  ovolicc1  25451  ioombl1lem1  25493  dyadf  25526  itg1addlem4  25634  limccnp2  25827  dvaddbr  25874  dvmulbr  25875  dvmulbrOLD  25876  dvcobr  25883  dvcobrOLD  25884  lhop1lem  25952  cxpcn3  26692  mpodvdsmulf1o  27138  dvdsmulf1o  27140  addsqnreup  27388  addsval  27910  mulsval  28053  tgjustc1  28456  tgjustc2  28457  tgelrnln  28611  numclwwlk1lem2f  30335  ofresid  32617  fsuppcurry1  32699  fsuppcurry2  32700  gsumpart  33041  gsumwrd2dccatlem  33050  gsumwrd2dccat  33051  elrgspnsubrunlem2  33216  erlbrd  33231  rlocaddval  33236  rlocmulval  33237  rloccring  33238  rloc0g  33239  rloc1r  33240  rlocf1  33241  fracerl  33273  fracfld  33275  zringfrac  33519  prsdm  33898  prsrn  33899  esum2dlem  34076  hgt750lemb  34641  cvmlift2lem10  35293  goelel3xp  35329  sat1el2xp  35360  fmla0xp  35364  prv1n  35412  pprodss4v  35866  poimirlem3  37611  poimirlem4  37612  poimirlem17  37625  poimirlem20  37628  mblfinlem2  37646  aks6d1c3  42105  aks6d1c7lem1  42162  f1o2d2  42215  projf1o  45185  ovolval4lem1  46641  ovolval5lem2  46645  gpgiedgdmellem  48031  gpgvtx0  48038  gpgvtx1  48039  gpg3kgrtriex  48074  gpgprismgr4cycllem3  48081  gpgprismgr4cycllem9  48087  tposidres  48868  oppf1st2nd  49114  imaid  49137  xpcfuccocl  49240  swapf1  49255  swapf2val  49256  swapf2  49257  cofuswapf1  49277  cofuswapf2  49278  lanfval  49596  ranfval  49597