Theorem opelxpd 5689

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ⟨cop 4589   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-opab 5167  df-xp 5656

This theorem is used by:  otel3xp  5696  opabssxpd  5697  relssdmrn  6271  fpr2g  7217  fliftrel  7316  elovimad  7470  el2xptp0  8047  oprab2co  8108  1stconst  8111  2ndconst  8112  curry2  8118  fsplitfpar  8129  offsplitfpar  8130  mpof1o2d  8137  fnwelem  8143  xpf1o  9158  xpmapenlem  9163  unxpdomlem3  9249  fseqenlem1  10103  fseqenlem2  10104  iundom2g  10624  ordpipq  11027  addpqf  11029  mulpqf  11031  recmulnq  11049  ltexnq  11060  axmulf  11231  cnrecnv  15332  ruclem1  16399  eucalgf  16758  qredeu  16833  crth  16955  phimullem  16956  prmreclem3  17096  setsstruct2  17352  imasaddflem  17702  xpsaddlem  17745  xpsvsca  17749  xpsle  17751  comffval  17873  oppccofval  17890  isoval  17940  brcic  17973  funcf2  18043  idfu2nd  18052  resf2nd  18070  wunfunc  18076  homaval  18206  setcco  18258  catcco  18280  estrcco  18304  xpcco  18357  xpchom2  18360  xpcco2  18361  xpccatid  18362  prfcl  18377  prf1st  18378  prf2nd  18379  evlf2  18392  curf1cl  18402  curf2cl  18405  curfcl  18406  uncf1  18410  uncf2  18411  uncfcurf  18413  diag11  18417  diag12  18418  diag2  18419  curf2ndf  18421  hof2fval  18429  yonedalem21  18447  yonedalem22  18452  yonedalem3b  18453  yonffthlem  18456  latcl2  18610  xpsmnd0  18972  xpsinv  19270  xpsgrpsub  19271  lsmhash  19919  frgpuplem  19986  xpsring1d  20563  rngqiprngimf  21593  pzriprnglem4  21790  pzriprnglem5  21791  pzriprnglem8  21794  pzriprnglem12  21798  mdetrlin  22917  mdetrsca  22918  txcls  23923  txcnp  23939  txcnmpt  23943  txdis1cn  23954  txlly  23955  txnlly  23956  txlm  23967  lmcn2  23968  txkgen  23971  xkococnlem  23978  txhmeo  24122  ptuncnv  24126  txflf  24325  flfcnp2  24326  tmdcn2  24408  qustgplem  24440  tsmsadd  24466  imasdsf1olem  24692  xpsdsval  24700  comet  24832  metustid  24873  metustexhalf  24875  metuel2  24884  tngnm  24970  cnheiborlem  25275  bcthlem5  25649  ovollb2lem  25809  ovolctb  25811  ovoliunlem2  25824  ovolshftlem1  25830  ovolscalem1  25834  ovolicc1  25837  ioombl1lem1  25879  dyadf  25912  itg1addlem4  26020  limccnp2  26212  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  lhop1lem  26333  cxpcn3  27076  mpodvdsmulf1o  27521  dvdsmulf1o  27523  addsqnreup  27770  addsval  28348  mulsval  28495  tgjustc1  28937  tgjustc2  28938  tgelrnln  29098  tgelrnpln  29254  numclwwlk1lem2f  30956  ofresid  33236  fsuppcurry1  33316  fsuppcurry2  33317  gsumpart  33624  gsumwrd2dccatlem  33638  gsumwrd2dccat  33639  elrgspnsubrunlem2  33809  erlbrd  33824  erld2  33827  rlocaddval  33830  rlocmulval  33831  rloccring  33832  rloc0g  33833  rloc1r  33834  rlocf1  33835  rlocinvunit  33836  rlocisunit  33837  fracerl  33868  fracfld  33870  zringfrac  34086  prsdm  34546  prsrn  34547  esum2dlem  34724  hgt750lemb  35285  cvmlift2lem10  36077  goelel3xp  36113  sat1el2xp  36144  fmla0xp  36148  prv1n  36196  pprodss4v  36646  nmulprop  36939  poimirlem3  38542  poimirlem4  38543  poimirlem17  38556  poimirlem20  38559  mblfinlem2  38577  aks6d1c3  43174  aks6d1c7lem1  43231  projf1o  46211  hoicvr  47558  ovolval4lem1  47659  ovolval5lem2  47663  gpgiedgdmellem  49144  gpgvtx0  49151  gpgvtx1  49152  gpg3kgrtriex  49187  gpgprismgr4cycllem3  49195  gpgprismgr4cycllem9  49201  tposidres  49994  oppf1st2nd  50239  imaid  50262  xpcfuccocl  50365  swapf1  50380  swapf2val  50381  swapf2  50382  cofuswapf1  50402  cofuswapf2  50403  lanfval  50721  ranfval  50722