Theorem opelxpd 5687

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ⟨cop 4590   × cxp 5646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5654

This theorem is used by:  otel3xp  5694  opabssxpd  5695  relssdmrn  6261  fpr2g  7206  fliftrel  7305  elovimad  7459  el2xptp0  8031  oprab2co  8092  1stconst  8095  2ndconst  8096  curry2  8102  fsplitfpar  8113  offsplitfpar  8114  mpof1o2d  8121  fnwelem  8127  xpf1o  9137  xpmapenlem  9142  unxpdomlem3  9228  fseqenlem1  10060  fseqenlem2  10061  iundom2g  10581  ordpipq  10984  addpqf  10986  mulpqf  10988  recmulnq  11006  ltexnq  11017  axmulf  11188  cnrecnv  15285  ruclem1  16352  eucalgf  16706  qredeu  16781  crth  16902  phimullem  16903  prmreclem3  17043  setsstruct2  17299  imasaddflem  17649  xpsaddlem  17692  xpsvsca  17696  xpsle  17698  comffval  17820  oppccofval  17837  isoval  17887  brcic  17920  funcf2  17990  idfu2nd  17999  resf2nd  18017  wunfunc  18023  homaval  18153  setcco  18205  catcco  18227  estrcco  18251  xpcco  18304  xpchom2  18307  xpcco2  18308  xpccatid  18309  prfcl  18324  prf1st  18325  prf2nd  18326  evlf2  18339  curf1cl  18349  curf2cl  18352  curfcl  18353  uncf1  18357  uncf2  18358  uncfcurf  18360  diag11  18364  diag12  18365  diag2  18366  curf2ndf  18368  hof2fval  18376  yonedalem21  18394  yonedalem22  18399  yonedalem3b  18400  yonffthlem  18403  latcl2  18557  xpsmnd0  18919  xpsinv  19217  xpsgrpsub  19218  lsmhash  19866  frgpuplem  19933  xpsring1d  20510  rngqiprngimf  21540  pzriprnglem4  21737  pzriprnglem5  21738  pzriprnglem8  21741  pzriprnglem12  21745  mdetrlin  22864  mdetrsca  22865  txcls  23870  txcnp  23886  txcnmpt  23890  txdis1cn  23901  txlly  23902  txnlly  23903  txlm  23914  lmcn2  23915  txkgen  23918  xkococnlem  23925  txhmeo  24069  ptuncnv  24073  txflf  24272  flfcnp2  24273  tmdcn2  24355  qustgplem  24387  tsmsadd  24413  imasdsf1olem  24639  xpsdsval  24647  comet  24779  metustid  24820  metustexhalf  24822  metuel2  24831  tngnm  24917  cnheiborlem  25222  bcthlem5  25596  ovollb2lem  25756  ovolctb  25758  ovoliunlem2  25771  ovolshftlem1  25777  ovolscalem1  25781  ovolicc1  25784  ioombl1lem1  25826  dyadf  25859  itg1addlem4  25967  limccnp2  26159  dvaddbr  26205  dvmulbr  26206  dvcobr  26213  lhop1lem  26280  cxpcn3  27025  mpodvdsmulf1o  27470  dvdsmulf1o  27472  addsqnreup  27719  addsval  28267  mulsval  28414  tgjustc1  28856  tgjustc2  28857  tgelrnln  29017  tgelrnpln  29173  numclwwlk1lem2f  30875  ofresid  33155  fsuppcurry1  33235  fsuppcurry2  33236  gsumpart  33543  gsumwrd2dccatlem  33557  gsumwrd2dccat  33558  elrgspnsubrunlem2  33728  erlbrd  33743  erld2  33746  rlocaddval  33749  rlocmulval  33750  rloccring  33751  rloc0g  33752  rloc1r  33753  rlocf1  33754  rlocinvunit  33755  rlocisunit  33756  fracerl  33787  fracfld  33789  zringfrac  34005  prsdm  34465  prsrn  34466  esum2dlem  34643  hgt750lemb  35205  cvmlift2lem10  35992  goelel3xp  36028  sat1el2xp  36059  fmla0xp  36063  prv1n  36111  pprodss4v  36562  nmulprop  36855  poimirlem3  38455  poimirlem4  38456  poimirlem17  38469  poimirlem20  38472  mblfinlem2  38490  aks6d1c3  43087  aks6d1c7lem1  43144  projf1o  46126  hoicvr  47474  ovolval4lem1  47575  ovolval5lem2  47579  gpgiedgdmellem  49060  gpgvtx0  49067  gpgvtx1  49068  gpg3kgrtriex  49103  gpgprismgr4cycllem3  49111  gpgprismgr4cycllem9  49117  tposidres  49910  oppf1st2nd  50155  imaid  50178  xpcfuccocl  50281  swapf1  50296  swapf2val  50297  swapf2  50298  cofuswapf1  50318  cofuswapf2  50319  lanfval  50637  ranfval  50638