Theorem opelxpd 5670

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

Syntax hints:   → wi 4   ∈ wcel 2109  ⟨cop 4591   × cxp 5629

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637

This theorem is referenced by:  otel3xp  5677  opabssxpd  5678  relssdmrn  6229  fpr2g  7167  fliftrel  7265  elovimad  7419  el2xptp0  7994  oprab2co  8053  1stconst  8056  2ndconst  8057  curry2  8063  fsplitfpar  8074  offsplitfpar  8075  fnwelem  8087  xpf1o  9080  xpmapenlem  9085  unxpdomlem3  9175  fseqenlem1  9953  fseqenlem2  9954  iundom2g  10469  ordpipq  10871  addpqf  10873  mulpqf  10875  recmulnq  10893  ltexnq  10904  axmulf  11075  cnrecnv  15107  ruclem1  16175  eucalgf  16529  qredeu  16604  crth  16724  phimullem  16725  prmreclem3  16865  setsstruct2  17120  imasaddflem  17469  xpsaddlem  17512  xpsvsca  17516  xpsle  17518  comffval  17640  oppccofval  17657  isoval  17707  brcic  17740  funcf2  17810  idfu2nd  17819  resf2nd  17837  wunfunc  17843  homaval  17973  setcco  18025  catcco  18047  estrcco  18071  xpcco  18124  xpchom2  18127  xpcco2  18128  xpccatid  18129  prfcl  18144  prf1st  18145  prf2nd  18146  evlf2  18159  curf1cl  18169  curf2cl  18172  curfcl  18173  uncf1  18177  uncf2  18178  uncfcurf  18180  diag11  18184  diag12  18185  diag2  18186  curf2ndf  18188  hof2fval  18196  yonedalem21  18214  yonedalem22  18219  yonedalem3b  18220  yonffthlem  18223  latcl2  18377  xpsmnd0  18687  xpsinv  18974  xpsgrpsub  18975  lsmhash  19619  frgpuplem  19686  xpsring1d  20253  rngqiprngimf  21239  pzriprnglem4  21426  pzriprnglem5  21427  pzriprnglem8  21430  pzriprnglem12  21434  mdetrlin  22522  mdetrsca  22523  txcls  23524  txcnp  23540  txcnmpt  23544  txdis1cn  23555  txlly  23556  txnlly  23557  txlm  23568  lmcn2  23569  txkgen  23572  xkococnlem  23579  txhmeo  23723  ptuncnv  23727  txflf  23926  flfcnp2  23927  tmdcn2  24009  qustgplem  24041  tsmsadd  24067  imasdsf1olem  24294  xpsdsval  24302  comet  24434  metustid  24475  metustexhalf  24477  metuel2  24486  tngnm  24572  cnheiborlem  24886  bcthlem5  25261  ovollb2lem  25422  ovolctb  25424  ovoliunlem2  25437  ovolshftlem1  25443  ovolscalem1  25447  ovolicc1  25450  ioombl1lem1  25492  dyadf  25525  itg1addlem4  25633  limccnp2  25826  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  lhop1lem  25951  cxpcn3  26691  mpodvdsmulf1o  27137  dvdsmulf1o  27139  addsqnreup  27387  addsval  27909  mulsval  28052  tgjustc1  28455  tgjustc2  28456  tgelrnln  28610  numclwwlk1lem2f  30334  ofresid  32616  fsuppcurry1  32698  fsuppcurry2  32699  gsumpart  33040  gsumwrd2dccatlem  33049  gsumwrd2dccat  33050  elrgspnsubrunlem2  33215  erlbrd  33230  rlocaddval  33235  rlocmulval  33236  rloccring  33237  rloc0g  33238  rloc1r  33239  rlocf1  33240  fracerl  33272  fracfld  33274  zringfrac  33518  prsdm  33897  prsrn  33898  esum2dlem  34075  hgt750lemb  34640  cvmlift2lem10  35292  goelel3xp  35328  sat1el2xp  35359  fmla0xp  35363  prv1n  35411  pprodss4v  35865  poimirlem3  37610  poimirlem4  37611  poimirlem17  37624  poimirlem20  37627  mblfinlem2  37645  aks6d1c3  42104  aks6d1c7lem1  42161  f1o2d2  42214  projf1o  45184  ovolval4lem1  46640  ovolval5lem2  46644  gpgiedgdmellem  48030  gpgvtx0  48037  gpgvtx1  48038  gpg3kgrtriex  48073  gpgprismgr4cycllem3  48080  gpgprismgr4cycllem9  48086  tposidres  48867  oppf1st2nd  49113  imaid  49136  xpcfuccocl  49239  swapf1  49254  swapf2val  49255  swapf2  49256  cofuswapf1  49276  cofuswapf2  49277  lanfval  49595  ranfval  49596