Theorem opelxpd 5574

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

Syntax hints:   → wi 4   ∈ wcel 2112  ⟨cop 4533   × cxp 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-opab 5102  df-xp 5542

This theorem is referenced by:  otel3xp  5580  opabssxpd  5581  fpr2g  7005  fliftrel  7095  elovimad  7239  el2xptp0  7786  oprab2co  7843  1stconst  7846  2ndconst  7847  curry2  7853  fsplitfpar  7865  offsplitfpar  7866  fnwelem  7876  xpf1o  8786  xpmapenlem  8791  unxpdomlem3  8860  fseqenlem1  9603  fseqenlem2  9604  iundom2g  10119  ordpipq  10521  addpqf  10523  mulpqf  10525  recmulnq  10543  ltexnq  10554  axmulf  10725  cnrecnv  14693  ruclem1  15755  eucalgf  16103  qredeu  16178  crth  16294  phimullem  16295  prmreclem3  16434  setsstruct2  16703  imasaddflem  16989  xpsaddlem  17032  xpsvsca  17036  xpsle  17038  comffval  17156  oppccofval  17174  isoval  17224  brcic  17257  funcf2  17328  idfu2nd  17337  resf2nd  17355  wunfunc  17359  wunfuncOLD  17360  homaval  17491  setcco  17543  catcco  17565  estrcco  17591  xpcco  17644  xpchom2  17647  xpcco2  17648  xpccatid  17649  prfcl  17664  prf1st  17665  prf2nd  17666  evlf2  17680  curf1cl  17690  curf2cl  17693  curfcl  17694  uncf1  17698  uncf2  17699  uncfcurf  17701  diag11  17705  diag12  17706  diag2  17707  curf2ndf  17709  hof2fval  17717  yonedalem21  17735  yonedalem22  17740  yonedalem3b  17741  yonffthlem  17744  latcl2  17896  lsmhash  19049  frgpuplem  19116  mdetrlin  21453  mdetrsca  21454  txcls  22455  txcnp  22471  txcnmpt  22475  txdis1cn  22486  txlly  22487  txnlly  22488  txlm  22499  lmcn2  22500  txkgen  22503  xkococnlem  22510  txhmeo  22654  ptuncnv  22658  txflf  22857  flfcnp2  22858  tmdcn2  22940  qustgplem  22972  tsmsadd  22998  imasdsf1olem  23225  xpsdsval  23233  comet  23365  metustid  23406  metustexhalf  23408  metuel2  23417  tngnm  23503  cnheiborlem  23805  bcthlem5  24179  ovollb2lem  24339  ovolctb  24341  ovoliunlem2  24354  ovolshftlem1  24360  ovolscalem1  24364  ovolicc1  24367  ioombl1lem1  24409  dyadf  24442  itg1addlem4  24550  itg1addlem4OLD  24551  limccnp2  24743  dvaddbr  24789  dvmulbr  24790  dvcobr  24797  lhop1lem  24864  cxpcn3  25588  dvdsmulf1o  26030  addsqnreup  26278  tgjustc1  26520  tgjustc2  26521  tgelrnln  26675  numclwwlk1lem2f  28392  ofresid  30652  fsuppcurry1  30734  fsuppcurry2  30735  gsumpart  30988  prsdm  31532  prsrn  31533  esum2dlem  31726  hgt750lemb  32302  cvmlift2lem10  32941  goelel3xp  32977  sat1el2xp  33008  fmla0xp  33012  prv1n  33060  addsval  33812  pprodss4v  33872  poimirlem3  35466  poimirlem4  35467  poimirlem17  35480  poimirlem20  35483  mblfinlem2  35501  projf1o  42350  ovolval4lem1  43805  ovolval5lem2  43809