Theorem opelxpd 5680

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

Syntax hints:   → wi 4   ∈ wcel 2109  ⟨cop 4598   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-xp 5647

This theorem is referenced by:  otel3xp  5687  opabssxpd  5688  relssdmrn  6244  fpr2g  7188  fliftrel  7286  elovimad  7440  el2xptp0  8018  oprab2co  8079  1stconst  8082  2ndconst  8083  curry2  8089  fsplitfpar  8100  offsplitfpar  8101  fnwelem  8113  xpf1o  9109  xpmapenlem  9114  unxpdomlem3  9206  fseqenlem1  9984  fseqenlem2  9985  iundom2g  10500  ordpipq  10902  addpqf  10904  mulpqf  10906  recmulnq  10924  ltexnq  10935  axmulf  11106  cnrecnv  15138  ruclem1  16206  eucalgf  16560  qredeu  16635  crth  16755  phimullem  16756  prmreclem3  16896  setsstruct2  17151  imasaddflem  17500  xpsaddlem  17543  xpsvsca  17547  xpsle  17549  comffval  17667  oppccofval  17684  isoval  17734  brcic  17767  funcf2  17837  idfu2nd  17846  resf2nd  17864  wunfunc  17870  homaval  18000  setcco  18052  catcco  18074  estrcco  18098  xpcco  18151  xpchom2  18154  xpcco2  18155  xpccatid  18156  prfcl  18171  prf1st  18172  prf2nd  18173  evlf2  18186  curf1cl  18196  curf2cl  18199  curfcl  18200  uncf1  18204  uncf2  18205  uncfcurf  18207  diag11  18211  diag12  18212  diag2  18213  curf2ndf  18215  hof2fval  18223  yonedalem21  18241  yonedalem22  18246  yonedalem3b  18247  yonffthlem  18250  latcl2  18402  xpsmnd0  18712  xpsinv  18999  xpsgrpsub  19000  lsmhash  19642  frgpuplem  19709  xpsring1d  20249  rngqiprngimf  21214  pzriprnglem4  21401  pzriprnglem5  21402  pzriprnglem8  21405  pzriprnglem12  21409  mdetrlin  22496  mdetrsca  22497  txcls  23498  txcnp  23514  txcnmpt  23518  txdis1cn  23529  txlly  23530  txnlly  23531  txlm  23542  lmcn2  23543  txkgen  23546  xkococnlem  23553  txhmeo  23697  ptuncnv  23701  txflf  23900  flfcnp2  23901  tmdcn2  23983  qustgplem  24015  tsmsadd  24041  imasdsf1olem  24268  xpsdsval  24276  comet  24408  metustid  24449  metustexhalf  24451  metuel2  24460  tngnm  24546  cnheiborlem  24860  bcthlem5  25235  ovollb2lem  25396  ovolctb  25398  ovoliunlem2  25411  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ioombl1lem1  25466  dyadf  25499  itg1addlem4  25607  limccnp2  25800  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  lhop1lem  25925  cxpcn3  26665  mpodvdsmulf1o  27111  dvdsmulf1o  27113  addsqnreup  27361  addsval  27876  mulsval  28019  tgjustc1  28409  tgjustc2  28410  tgelrnln  28564  numclwwlk1lem2f  30291  ofresid  32573  fsuppcurry1  32655  fsuppcurry2  32656  gsumpart  33004  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  elrgspnsubrunlem2  33206  erlbrd  33221  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  fracerl  33263  fracfld  33265  zringfrac  33532  prsdm  33911  prsrn  33912  esum2dlem  34089  hgt750lemb  34654  cvmlift2lem10  35306  goelel3xp  35342  sat1el2xp  35373  fmla0xp  35377  prv1n  35425  pprodss4v  35879  poimirlem3  37624  poimirlem4  37625  poimirlem17  37638  poimirlem20  37641  mblfinlem2  37659  aks6d1c3  42118  aks6d1c7lem1  42175  f1o2d2  42228  projf1o  45198  ovolval4lem1  46654  ovolval5lem2  46658  gpgiedgdmellem  48041  gpgvtx0  48048  gpgvtx1  48049  gpg3kgrtriex  48084  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem9  48097  tposidres  48878  oppf1st2nd  49124  imaid  49147  xpcfuccocl  49250  swapf1  49265  swapf2val  49266  swapf2  49267  cofuswapf1  49287  cofuswapf2  49288  lanfval  49606  ranfval  49607