Theorem opelxpd 5716

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

Syntax hints:   → wi 4   ∈ wcel 2107  ⟨cop 4635   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-xp 5683

This theorem is referenced by:  otel3xp  5723  opabssxpd  5724  relssdmrn  6268  fpr2g  7213  fliftrel  7305  elovimad  7457  el2xptp0  8022  oprab2co  8083  1stconst  8086  2ndconst  8087  curry2  8093  fsplitfpar  8104  offsplitfpar  8105  fnwelem  8117  xpf1o  9139  xpmapenlem  9144  unxpdomlem3  9252  fseqenlem1  10019  fseqenlem2  10020  iundom2g  10535  ordpipq  10937  addpqf  10939  mulpqf  10941  recmulnq  10959  ltexnq  10970  axmulf  11141  cnrecnv  15112  ruclem1  16174  eucalgf  16520  qredeu  16595  crth  16711  phimullem  16712  prmreclem3  16851  setsstruct2  17107  imasaddflem  17476  xpsaddlem  17519  xpsvsca  17523  xpsle  17525  comffval  17643  oppccofval  17661  isoval  17712  brcic  17745  funcf2  17818  idfu2nd  17827  resf2nd  17845  wunfunc  17849  wunfuncOLD  17850  homaval  17981  setcco  18033  catcco  18055  estrcco  18081  xpcco  18135  xpchom2  18138  xpcco2  18139  xpccatid  18140  prfcl  18155  prf1st  18156  prf2nd  18157  evlf2  18171  curf1cl  18181  curf2cl  18184  curfcl  18185  uncf1  18189  uncf2  18190  uncfcurf  18192  diag11  18196  diag12  18197  diag2  18198  curf2ndf  18200  hof2fval  18208  yonedalem21  18226  yonedalem22  18231  yonedalem3b  18232  yonffthlem  18235  latcl2  18389  xpsmnd0  18666  xpsinv  18943  xpsgrpsub  18944  lsmhash  19573  frgpuplem  19640  xpsring1d  20146  mdetrlin  22104  mdetrsca  22105  txcls  23108  txcnp  23124  txcnmpt  23128  txdis1cn  23139  txlly  23140  txnlly  23141  txlm  23152  lmcn2  23153  txkgen  23156  xkococnlem  23163  txhmeo  23307  ptuncnv  23311  txflf  23510  flfcnp2  23511  tmdcn2  23593  qustgplem  23625  tsmsadd  23651  imasdsf1olem  23879  xpsdsval  23887  comet  24022  metustid  24063  metustexhalf  24065  metuel2  24074  tngnm  24168  cnheiborlem  24470  bcthlem5  24845  ovollb2lem  25005  ovolctb  25007  ovoliunlem2  25020  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ioombl1lem1  25075  dyadf  25108  itg1addlem4  25216  itg1addlem4OLD  25217  limccnp2  25409  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  lhop1lem  25530  cxpcn3  26256  dvdsmulf1o  26698  addsqnreup  26946  addsval  27448  mulsval  27568  tgjustc1  27757  tgjustc2  27758  tgelrnln  27912  numclwwlk1lem2f  29639  ofresid  31898  fsuppcurry1  31981  fsuppcurry2  31982  gsumpart  32238  prsdm  32925  prsrn  32926  esum2dlem  33121  hgt750lemb  33699  cvmlift2lem10  34334  goelel3xp  34370  sat1el2xp  34401  fmla0xp  34405  prv1n  34453  pprodss4v  34887  gg-dvmulbr  35206  gg-dvcobr  35207  poimirlem3  36539  poimirlem4  36540  poimirlem17  36553  poimirlem20  36556  mblfinlem2  36574  f1o2d2  41103  projf1o  43944  ovolval4lem1  45413  ovolval5lem2  45417  rngqiprngimf  46830  pzriprnglem4  46856  pzriprnglem5  46857  pzriprnglem8  46860  pzriprnglem12  46864