Theorem opelxpd 5708

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

Syntax hints:   → wi 4   ∈ wcel 2098  ⟨cop 4629   × cxp 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-opab 5204  df-xp 5675

This theorem is referenced by:  otel3xp  5715  opabssxpd  5716  relssdmrn  6261  fpr2g  7208  fliftrel  7301  elovimad  7453  el2xptp0  8021  oprab2co  8083  1stconst  8086  2ndconst  8087  curry2  8093  fsplitfpar  8104  offsplitfpar  8105  fnwelem  8117  xpf1o  9141  xpmapenlem  9146  unxpdomlem3  9254  fseqenlem1  10021  fseqenlem2  10022  iundom2g  10537  ordpipq  10939  addpqf  10941  mulpqf  10943  recmulnq  10961  ltexnq  10972  axmulf  11143  cnrecnv  15118  ruclem1  16181  eucalgf  16527  qredeu  16602  crth  16720  phimullem  16721  prmreclem3  16860  setsstruct2  17116  imasaddflem  17485  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  comffval  17652  oppccofval  17670  isoval  17721  brcic  17754  funcf2  17827  idfu2nd  17836  resf2nd  17854  wunfunc  17860  wunfuncOLD  17861  homaval  17993  setcco  18045  catcco  18067  estrcco  18093  xpcco  18147  xpchom2  18150  xpcco2  18151  xpccatid  18152  prfcl  18167  prf1st  18168  prf2nd  18169  evlf2  18183  curf1cl  18193  curf2cl  18196  curfcl  18197  uncf1  18201  uncf2  18202  uncfcurf  18204  diag11  18208  diag12  18209  diag2  18210  curf2ndf  18212  hof2fval  18220  yonedalem21  18238  yonedalem22  18243  yonedalem3b  18244  yonffthlem  18247  latcl2  18401  xpsmnd0  18708  xpsinv  18988  xpsgrpsub  18989  lsmhash  19625  frgpuplem  19692  xpsring1d  20232  rngqiprngimf  21150  pzriprnglem4  21371  pzriprnglem5  21372  pzriprnglem8  21375  pzriprnglem12  21379  mdetrlin  22459  mdetrsca  22460  txcls  23463  txcnp  23479  txcnmpt  23483  txdis1cn  23494  txlly  23495  txnlly  23496  txlm  23507  lmcn2  23508  txkgen  23511  xkococnlem  23518  txhmeo  23662  ptuncnv  23666  txflf  23865  flfcnp2  23866  tmdcn2  23948  qustgplem  23980  tsmsadd  24006  imasdsf1olem  24234  xpsdsval  24242  comet  24377  metustid  24418  metustexhalf  24420  metuel2  24429  tngnm  24523  cnheiborlem  24835  bcthlem5  25211  ovollb2lem  25372  ovolctb  25374  ovoliunlem2  25387  ovolshftlem1  25393  ovolscalem1  25397  ovolicc1  25400  ioombl1lem1  25442  dyadf  25475  itg1addlem4  25583  itg1addlem4OLD  25584  limccnp2  25776  dvaddbr  25823  dvmulbr  25824  dvmulbrOLD  25825  dvcobr  25832  dvcobrOLD  25833  lhop1lem  25901  cxpcn3  26638  mpodvdsmulf1o  27081  dvdsmulf1o  27083  addsqnreup  27331  addsval  27834  mulsval  27964  tgjustc1  28234  tgjustc2  28235  tgelrnln  28389  numclwwlk1lem2f  30117  ofresid  32376  fsuppcurry1  32457  fsuppcurry2  32458  gsumpart  32713  prsdm  33424  prsrn  33425  esum2dlem  33620  hgt750lemb  34197  cvmlift2lem10  34831  goelel3xp  34867  sat1el2xp  34898  fmla0xp  34902  prv1n  34950  pprodss4v  35389  poimirlem3  37004  poimirlem4  37005  poimirlem17  37018  poimirlem20  37021  mblfinlem2  37039  aks6d1c3  41501  f1o2d2  41621  projf1o  44473  ovolval4lem1  45942  ovolval5lem2  45946