Theorem opelxpd 5688

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

Syntax hints:   → wi 4   ∈ wcel 2144  ⟨cop 4590   × cxp 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5165  df-xp 5655

This theorem is referenced by:  otel3xp  5695  opabssxpd  5696  relssdmrn  6258  fpr2g  7197  fliftrel  7294  elovimad  7448  el2xptp0  8019  oprab2co  8078  1stconst  8081  2ndconst  8082  curry2  8088  fsplitfpar  8099  offsplitfpar  8100  mpof1o2d  8107  fnwelem  8113  xpf1o  9113  xpmapenlem  9118  unxpdomlem3  9204  fseqenlem1  9982  fseqenlem2  9983  iundom2g  10499  ordpipq  10902  addpqf  10904  mulpqf  10906  recmulnq  10924  ltexnq  10935  axmulf  11106  cnrecnv  15194  ruclem1  16265  eucalgf  16619  qredeu  16694  crth  16815  phimullem  16816  prmreclem3  16956  setsstruct2  17212  imasaddflem  17562  xpsaddlem  17605  xpsvsca  17609  xpsle  17611  comffval  17733  oppccofval  17750  isoval  17800  brcic  17833  funcf2  17903  idfu2nd  17912  resf2nd  17930  wunfunc  17936  homaval  18066  setcco  18118  catcco  18140  estrcco  18164  xpcco  18217  xpchom2  18220  xpcco2  18221  xpccatid  18222  prfcl  18237  prf1st  18238  prf2nd  18239  evlf2  18252  curf1cl  18262  curf2cl  18265  curfcl  18266  uncf1  18270  uncf2  18271  uncfcurf  18273  diag11  18277  diag12  18278  diag2  18279  curf2ndf  18281  hof2fval  18289  yonedalem21  18307  yonedalem22  18312  yonedalem3b  18313  yonffthlem  18316  latcl2  18470  xpsmnd0  18814  xpsinv  19104  xpsgrpsub  19105  lsmhash  19747  frgpuplem  19814  xpsring1d  20384  rngqiprngimf  21369  pzriprnglem4  21538  pzriprnglem5  21539  pzriprnglem8  21542  pzriprnglem12  21546  mdetrlin  22664  mdetrsca  22665  txcls  23666  txcnp  23682  txcnmpt  23686  txdis1cn  23697  txlly  23698  txnlly  23699  txlm  23710  lmcn2  23711  txkgen  23714  xkococnlem  23721  txhmeo  23865  ptuncnv  23869  txflf  24068  flfcnp2  24069  tmdcn2  24151  qustgplem  24183  tsmsadd  24209  imasdsf1olem  24435  xpsdsval  24443  comet  24575  metustid  24616  metustexhalf  24618  metuel2  24627  tngnm  24713  cnheiborlem  25018  bcthlem5  25392  ovollb2lem  25552  ovolctb  25554  ovoliunlem2  25567  ovolshftlem1  25573  ovolscalem1  25577  ovolicc1  25580  ioombl1lem1  25622  dyadf  25655  itg1addlem4  25763  limccnp2  25956  dvaddbr  26002  dvmulbr  26003  dvcobr  26010  lhop1lem  26077  cxpcn3  26815  mpodvdsmulf1o  27260  dvdsmulf1o  27262  addsqnreup  27509  addsval  28057  mulsval  28204  tgjustc1  28646  tgjustc2  28647  tgelrnln  28801  tgelrnpln  28985  numclwwlk1lem2f  30559  ofresid  32846  fsuppcurry1  32928  fsuppcurry2  32929  gsumpart  33245  gsumwrd2dccatlem  33259  gsumwrd2dccat  33260  elrgspnsubrunlem2  33431  erlbrd  33446  erld2  33449  rlocaddval  33452  rlocmulval  33453  rloccring  33454  rloc0g  33455  rloc1r  33456  rlocf1  33457  rlocinvunit  33458  rlocisunit  33459  fracerl  33495  fracfld  33497  zringfrac  33752  prsdm  34213  prsrn  34214  esum2dlem  34391  hgt750lemb  34952  cvmlift2lem10  35667  goelel3xp  35703  sat1el2xp  35734  fmla0xp  35738  prv1n  35786  pprodss4v  36237  nmulprop  36545  poimirlem3  38127  poimirlem4  38128  poimirlem17  38141  poimirlem20  38144  mblfinlem2  38162  aks6d1c3  42745  aks6d1c7lem1  42802  projf1o  45779  hoicvr  47127  ovolval4lem1  47228  ovolval5lem2  47232  gpgiedgdmellem  48673  gpgvtx0  48680  gpgvtx1  48681  gpg3kgrtriex  48716  gpgprismgr4cycllem3  48724  gpgprismgr4cycllem9  48730  tposidres  49512  oppf1st2nd  49757  imaid  49780  xpcfuccocl  49883  swapf1  49898  swapf2val  49899  swapf2  49900  cofuswapf1  49920  cofuswapf2  49921  lanfval  50239  ranfval  50240