Theorem opelxpd 5618

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟨cop 4564   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586

This theorem is referenced by:  otel3xp  5624  opabssxpd  5625  fpr2g  7069  fliftrel  7159  elovimad  7303  el2xptp0  7851  oprab2co  7908  1stconst  7911  2ndconst  7912  curry2  7918  fsplitfpar  7930  offsplitfpar  7931  fnwelem  7943  xpf1o  8875  xpmapenlem  8880  unxpdomlem3  8958  fseqenlem1  9711  fseqenlem2  9712  iundom2g  10227  ordpipq  10629  addpqf  10631  mulpqf  10633  recmulnq  10651  ltexnq  10662  axmulf  10833  cnrecnv  14804  ruclem1  15868  eucalgf  16216  qredeu  16291  crth  16407  phimullem  16408  prmreclem3  16547  setsstruct2  16803  imasaddflem  17158  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  comffval  17325  oppccofval  17343  isoval  17394  brcic  17427  funcf2  17499  idfu2nd  17508  resf2nd  17526  wunfunc  17530  wunfuncOLD  17531  homaval  17662  setcco  17714  catcco  17736  estrcco  17762  xpcco  17816  xpchom2  17819  xpcco2  17820  xpccatid  17821  prfcl  17836  prf1st  17837  prf2nd  17838  evlf2  17852  curf1cl  17862  curf2cl  17865  curfcl  17866  uncf1  17870  uncf2  17871  uncfcurf  17873  diag11  17877  diag12  17878  diag2  17879  curf2ndf  17881  hof2fval  17889  yonedalem21  17907  yonedalem22  17912  yonedalem3b  17913  yonffthlem  17916  latcl2  18069  lsmhash  19226  frgpuplem  19293  mdetrlin  21659  mdetrsca  21660  txcls  22663  txcnp  22679  txcnmpt  22683  txdis1cn  22694  txlly  22695  txnlly  22696  txlm  22707  lmcn2  22708  txkgen  22711  xkococnlem  22718  txhmeo  22862  ptuncnv  22866  txflf  23065  flfcnp2  23066  tmdcn2  23148  qustgplem  23180  tsmsadd  23206  imasdsf1olem  23434  xpsdsval  23442  comet  23575  metustid  23616  metustexhalf  23618  metuel2  23627  tngnm  23721  cnheiborlem  24023  bcthlem5  24397  ovollb2lem  24557  ovolctb  24559  ovoliunlem2  24572  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ioombl1lem1  24627  dyadf  24660  itg1addlem4  24768  itg1addlem4OLD  24769  limccnp2  24961  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  lhop1lem  25082  cxpcn3  25806  dvdsmulf1o  26248  addsqnreup  26496  tgjustc1  26740  tgjustc2  26741  tgelrnln  26895  numclwwlk1lem2f  28620  ofresid  30880  fsuppcurry1  30962  fsuppcurry2  30963  gsumpart  31217  prsdm  31766  prsrn  31767  esum2dlem  31960  hgt750lemb  32536  cvmlift2lem10  33174  goelel3xp  33210  sat1el2xp  33241  fmla0xp  33245  prv1n  33293  addsval  34053  pprodss4v  34113  poimirlem3  35707  poimirlem4  35708  poimirlem17  35721  poimirlem20  35724  mblfinlem2  35742  projf1o  42625  ovolval4lem1  44077  ovolval5lem2  44081