Theorem opelxpd 5627

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

Syntax hints:   → wi 4   ∈ wcel 2110  ⟨cop 4573   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5142  df-xp 5595

This theorem is referenced by:  otel3xp  5633  opabssxpd  5634  fpr2g  7082  fliftrel  7173  elovimad  7317  el2xptp0  7869  oprab2co  7926  1stconst  7929  2ndconst  7930  curry2  7936  fsplitfpar  7948  offsplitfpar  7949  fnwelem  7961  xpf1o  8906  xpmapenlem  8911  unxpdomlem3  9005  fseqenlem1  9779  fseqenlem2  9780  iundom2g  10295  ordpipq  10697  addpqf  10699  mulpqf  10701  recmulnq  10719  ltexnq  10730  axmulf  10901  cnrecnv  14872  ruclem1  15936  eucalgf  16284  qredeu  16359  crth  16475  phimullem  16476  prmreclem3  16615  setsstruct2  16871  imasaddflem  17237  xpsaddlem  17280  xpsvsca  17284  xpsle  17286  comffval  17404  oppccofval  17422  isoval  17473  brcic  17506  funcf2  17579  idfu2nd  17588  resf2nd  17606  wunfunc  17610  wunfuncOLD  17611  homaval  17742  setcco  17794  catcco  17816  estrcco  17842  xpcco  17896  xpchom2  17899  xpcco2  17900  xpccatid  17901  prfcl  17916  prf1st  17917  prf2nd  17918  evlf2  17932  curf1cl  17942  curf2cl  17945  curfcl  17946  uncf1  17950  uncf2  17951  uncfcurf  17953  diag11  17957  diag12  17958  diag2  17959  curf2ndf  17961  hof2fval  17969  yonedalem21  17987  yonedalem22  17992  yonedalem3b  17993  yonffthlem  17996  latcl2  18150  lsmhash  19307  frgpuplem  19374  mdetrlin  21747  mdetrsca  21748  txcls  22751  txcnp  22767  txcnmpt  22771  txdis1cn  22782  txlly  22783  txnlly  22784  txlm  22795  lmcn2  22796  txkgen  22799  xkococnlem  22806  txhmeo  22950  ptuncnv  22954  txflf  23153  flfcnp2  23154  tmdcn2  23236  qustgplem  23268  tsmsadd  23294  imasdsf1olem  23522  xpsdsval  23530  comet  23665  metustid  23706  metustexhalf  23708  metuel2  23717  tngnm  23811  cnheiborlem  24113  bcthlem5  24488  ovollb2lem  24648  ovolctb  24650  ovoliunlem2  24663  ovolshftlem1  24669  ovolscalem1  24673  ovolicc1  24676  ioombl1lem1  24718  dyadf  24751  itg1addlem4  24859  itg1addlem4OLD  24860  limccnp2  25052  dvaddbr  25098  dvmulbr  25099  dvcobr  25106  lhop1lem  25173  cxpcn3  25897  dvdsmulf1o  26339  addsqnreup  26587  tgjustc1  26832  tgjustc2  26833  tgelrnln  26987  numclwwlk1lem2f  28713  ofresid  30973  fsuppcurry1  31054  fsuppcurry2  31055  gsumpart  31309  prsdm  31858  prsrn  31859  esum2dlem  32054  hgt750lemb  32630  cvmlift2lem10  33268  goelel3xp  33304  sat1el2xp  33335  fmla0xp  33339  prv1n  33387  addsval  34120  pprodss4v  34180  poimirlem3  35774  poimirlem4  35775  poimirlem17  35788  poimirlem20  35791  mblfinlem2  35809  projf1o  42704  ovolval4lem1  44156  ovolval5lem2  44160