Theorem opelxpd 5739

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟨cop 4654   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-xp 5706

This theorem is referenced by:  otel3xp  5746  opabssxpd  5747  relssdmrn  6299  fpr2g  7248  fliftrel  7344  elovimad  7498  el2xptp0  8077  oprab2co  8138  1stconst  8141  2ndconst  8142  curry2  8148  fsplitfpar  8159  offsplitfpar  8160  fnwelem  8172  xpf1o  9205  xpmapenlem  9210  unxpdomlem3  9315  fseqenlem1  10093  fseqenlem2  10094  iundom2g  10609  ordpipq  11011  addpqf  11013  mulpqf  11015  recmulnq  11033  ltexnq  11044  axmulf  11215  cnrecnv  15214  ruclem1  16279  eucalgf  16630  qredeu  16705  crth  16825  phimullem  16826  prmreclem3  16965  setsstruct2  17221  imasaddflem  17590  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  comffval  17757  oppccofval  17775  isoval  17826  brcic  17859  funcf2  17932  idfu2nd  17941  resf2nd  17959  wunfunc  17965  wunfuncOLD  17966  homaval  18098  setcco  18150  catcco  18172  estrcco  18198  xpcco  18252  xpchom2  18255  xpcco2  18256  xpccatid  18257  prfcl  18272  prf1st  18273  prf2nd  18274  evlf2  18288  curf1cl  18298  curf2cl  18301  curfcl  18302  uncf1  18306  uncf2  18307  uncfcurf  18309  diag11  18313  diag12  18314  diag2  18315  curf2ndf  18317  hof2fval  18325  yonedalem21  18343  yonedalem22  18348  yonedalem3b  18349  yonffthlem  18352  latcl2  18506  xpsmnd0  18813  xpsinv  19100  xpsgrpsub  19101  lsmhash  19747  frgpuplem  19814  xpsring1d  20356  rngqiprngimf  21330  pzriprnglem4  21518  pzriprnglem5  21519  pzriprnglem8  21522  pzriprnglem12  21526  mdetrlin  22629  mdetrsca  22630  txcls  23633  txcnp  23649  txcnmpt  23653  txdis1cn  23664  txlly  23665  txnlly  23666  txlm  23677  lmcn2  23678  txkgen  23681  xkococnlem  23688  txhmeo  23832  ptuncnv  23836  txflf  24035  flfcnp2  24036  tmdcn2  24118  qustgplem  24150  tsmsadd  24176  imasdsf1olem  24404  xpsdsval  24412  comet  24547  metustid  24588  metustexhalf  24590  metuel2  24599  tngnm  24693  cnheiborlem  25005  bcthlem5  25381  ovollb2lem  25542  ovolctb  25544  ovoliunlem2  25557  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ioombl1lem1  25612  dyadf  25645  itg1addlem4  25753  itg1addlem4OLD  25754  limccnp2  25947  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  lhop1lem  26072  cxpcn3  26809  mpodvdsmulf1o  27255  dvdsmulf1o  27257  addsqnreup  27505  addsval  28013  mulsval  28153  tgjustc1  28501  tgjustc2  28502  tgelrnln  28656  numclwwlk1lem2f  30387  ofresid  32661  fsuppcurry1  32739  fsuppcurry2  32740  gsumpart  33038  erlbrd  33235  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rloc0g  33243  rloc1r  33244  rlocf1  33245  fracerl  33273  fracfld  33275  zringfrac  33547  prsdm  33860  prsrn  33861  esum2dlem  34056  hgt750lemb  34633  cvmlift2lem10  35280  goelel3xp  35316  sat1el2xp  35347  fmla0xp  35351  prv1n  35399  pprodss4v  35848  poimirlem3  37583  poimirlem4  37584  poimirlem17  37597  poimirlem20  37600  mblfinlem2  37618  aks6d1c3  42080  aks6d1c7lem1  42137  f1o2d2  42228  projf1o  45104  ovolval4lem1  46570  ovolval5lem2  46574