Theorem opelxpd 5667

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4574   × cxp 5626

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 2709  ax-sep 5232  ax-pr 5374

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5634

This theorem is referenced by:  otel3xp  5674  opabssxpd  5675  relssdmrn  6231  fpr2g  7163  fliftrel  7260  elovimad  7414  el2xptp0  7986  oprab2co  8044  1stconst  8047  2ndconst  8048  curry2  8054  fsplitfpar  8065  offsplitfpar  8066  fnwelem  8078  xpf1o  9074  xpmapenlem  9079  unxpdomlem3  9165  fseqenlem1  9943  fseqenlem2  9944  iundom2g  10459  ordpipq  10862  addpqf  10864  mulpqf  10866  recmulnq  10884  ltexnq  10895  axmulf  11066  cnrecnv  15124  ruclem1  16195  eucalgf  16549  qredeu  16624  crth  16745  phimullem  16746  prmreclem3  16886  setsstruct2  17141  imasaddflem  17491  xpsaddlem  17534  xpsvsca  17538  xpsle  17540  comffval  17662  oppccofval  17679  isoval  17729  brcic  17762  funcf2  17832  idfu2nd  17841  resf2nd  17859  wunfunc  17865  homaval  17995  setcco  18047  catcco  18069  estrcco  18093  xpcco  18146  xpchom2  18149  xpcco2  18150  xpccatid  18151  prfcl  18166  prf1st  18167  prf2nd  18168  evlf2  18181  curf1cl  18191  curf2cl  18194  curfcl  18195  uncf1  18199  uncf2  18200  uncfcurf  18202  diag11  18206  diag12  18207  diag2  18208  curf2ndf  18210  hof2fval  18218  yonedalem21  18236  yonedalem22  18241  yonedalem3b  18242  yonffthlem  18245  latcl2  18399  xpsmnd0  18743  xpsinv  19033  xpsgrpsub  19034  lsmhash  19677  frgpuplem  19744  xpsring1d  20310  rngqiprngimf  21293  pzriprnglem4  21480  pzriprnglem5  21481  pzriprnglem8  21484  pzriprnglem12  21488  mdetrlin  22583  mdetrsca  22584  txcls  23585  txcnp  23601  txcnmpt  23605  txdis1cn  23616  txlly  23617  txnlly  23618  txlm  23629  lmcn2  23630  txkgen  23633  xkococnlem  23640  txhmeo  23784  ptuncnv  23788  txflf  23987  flfcnp2  23988  tmdcn2  24070  qustgplem  24102  tsmsadd  24128  imasdsf1olem  24354  xpsdsval  24362  comet  24494  metustid  24535  metustexhalf  24537  metuel2  24546  tngnm  24632  cnheiborlem  24937  bcthlem5  25311  ovollb2lem  25471  ovolctb  25473  ovoliunlem2  25486  ovolshftlem1  25492  ovolscalem1  25496  ovolicc1  25499  ioombl1lem1  25541  dyadf  25574  itg1addlem4  25682  limccnp2  25875  dvaddbr  25921  dvmulbr  25922  dvcobr  25929  lhop1lem  25996  cxpcn3  26731  mpodvdsmulf1o  27177  dvdsmulf1o  27179  addsqnreup  27426  addsval  27974  mulsval  28121  tgjustc1  28563  tgjustc2  28564  tgelrnln  28718  numclwwlk1lem2f  30446  ofresid  32736  fsuppcurry1  32818  fsuppcurry2  32819  gsumpart  33145  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  elrgspnsubrunlem2  33330  erlbrd  33345  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  fracerl  33388  fracfld  33390  zringfrac  33635  prsdm  34080  prsrn  34081  esum2dlem  34258  hgt750lemb  34822  cvmlift2lem10  35516  goelel3xp  35552  sat1el2xp  35583  fmla0xp  35587  prv1n  35635  pprodss4v  36086  poimirlem3  37966  poimirlem4  37967  poimirlem17  37980  poimirlem20  37983  mblfinlem2  38001  aks6d1c3  42584  aks6d1c7lem1  42641  f1o2d2  42696  projf1o  45652  hoicvr  47002  ovolval4lem1  47103  ovolval5lem2  47107  gpgiedgdmellem  48542  gpgvtx0  48549  gpgvtx1  48550  gpg3kgrtriex  48585  gpgprismgr4cycllem3  48593  gpgprismgr4cycllem9  48599  tposidres  49381  oppf1st2nd  49626  imaid  49649  xpcfuccocl  49752  swapf1  49767  swapf2val  49768  swapf2  49769  cofuswapf1  49789  cofuswapf2  49790  lanfval  50108  ranfval  50109