Theorem opelxpd 5724

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟨cop 4632   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691

This theorem is referenced by:  otel3xp  5731  opabssxpd  5732  relssdmrn  6288  fpr2g  7231  fliftrel  7328  elovimad  7481  el2xptp0  8061  oprab2co  8122  1stconst  8125  2ndconst  8126  curry2  8132  fsplitfpar  8143  offsplitfpar  8144  fnwelem  8156  xpf1o  9179  xpmapenlem  9184  unxpdomlem3  9288  fseqenlem1  10064  fseqenlem2  10065  iundom2g  10580  ordpipq  10982  addpqf  10984  mulpqf  10986  recmulnq  11004  ltexnq  11015  axmulf  11186  cnrecnv  15204  ruclem1  16267  eucalgf  16620  qredeu  16695  crth  16815  phimullem  16816  prmreclem3  16956  setsstruct2  17211  imasaddflem  17575  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  comffval  17742  oppccofval  17759  isoval  17809  brcic  17842  funcf2  17913  idfu2nd  17922  resf2nd  17940  wunfunc  17946  homaval  18076  setcco  18128  catcco  18150  estrcco  18174  xpcco  18228  xpchom2  18231  xpcco2  18232  xpccatid  18233  prfcl  18248  prf1st  18249  prf2nd  18250  evlf2  18263  curf1cl  18273  curf2cl  18276  curfcl  18277  uncf1  18281  uncf2  18282  uncfcurf  18284  diag11  18288  diag12  18289  diag2  18290  curf2ndf  18292  hof2fval  18300  yonedalem21  18318  yonedalem22  18323  yonedalem3b  18324  yonffthlem  18327  latcl2  18481  xpsmnd0  18791  xpsinv  19078  xpsgrpsub  19079  lsmhash  19723  frgpuplem  19790  xpsring1d  20330  rngqiprngimf  21307  pzriprnglem4  21495  pzriprnglem5  21496  pzriprnglem8  21499  pzriprnglem12  21503  mdetrlin  22608  mdetrsca  22609  txcls  23612  txcnp  23628  txcnmpt  23632  txdis1cn  23643  txlly  23644  txnlly  23645  txlm  23656  lmcn2  23657  txkgen  23660  xkococnlem  23667  txhmeo  23811  ptuncnv  23815  txflf  24014  flfcnp2  24015  tmdcn2  24097  qustgplem  24129  tsmsadd  24155  imasdsf1olem  24383  xpsdsval  24391  comet  24526  metustid  24567  metustexhalf  24569  metuel2  24578  tngnm  24672  cnheiborlem  24986  bcthlem5  25362  ovollb2lem  25523  ovolctb  25525  ovoliunlem2  25538  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ioombl1lem1  25593  dyadf  25626  itg1addlem4  25734  limccnp2  25927  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  lhop1lem  26052  cxpcn3  26791  mpodvdsmulf1o  27237  dvdsmulf1o  27239  addsqnreup  27487  addsval  27995  mulsval  28135  tgjustc1  28483  tgjustc2  28484  tgelrnln  28638  numclwwlk1lem2f  30374  ofresid  32652  fsuppcurry1  32736  fsuppcurry2  32737  gsumpart  33060  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  elrgspnsubrunlem2  33252  erlbrd  33267  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  fracerl  33308  fracfld  33310  zringfrac  33582  prsdm  33913  prsrn  33914  esum2dlem  34093  hgt750lemb  34671  cvmlift2lem10  35317  goelel3xp  35353  sat1el2xp  35384  fmla0xp  35388  prv1n  35436  pprodss4v  35885  poimirlem3  37630  poimirlem4  37631  poimirlem17  37644  poimirlem20  37647  mblfinlem2  37665  aks6d1c3  42124  aks6d1c7lem1  42181  f1o2d2  42274  projf1o  45202  ovolval4lem1  46664  ovolval5lem2  46668  gpgedgel  48007  gpgvtx0  48008  gpgvtx1  48009  gpg3kgrtriex  48045  tposidres  48786  xpcfuccocl  48963  swapf1  48978  swapf2val  48979  swapf2  48980  cofuswapf1  48994  cofuswapf2  48995