Theorem opelxpd 5728

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

Syntax hints:   → wi 4   ∈ wcel 2106  ⟨cop 4637   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-xp 5695

This theorem is referenced by:  otel3xp  5735  opabssxpd  5736  relssdmrn  6290  fpr2g  7231  fliftrel  7328  elovimad  7481  el2xptp0  8060  oprab2co  8121  1stconst  8124  2ndconst  8125  curry2  8131  fsplitfpar  8142  offsplitfpar  8143  fnwelem  8155  xpf1o  9178  xpmapenlem  9183  unxpdomlem3  9286  fseqenlem1  10062  fseqenlem2  10063  iundom2g  10578  ordpipq  10980  addpqf  10982  mulpqf  10984  recmulnq  11002  ltexnq  11013  axmulf  11184  cnrecnv  15201  ruclem1  16264  eucalgf  16617  qredeu  16692  crth  16812  phimullem  16813  prmreclem3  16952  setsstruct2  17208  imasaddflem  17577  xpsaddlem  17620  xpsvsca  17624  xpsle  17626  comffval  17744  oppccofval  17762  isoval  17813  brcic  17846  funcf2  17919  idfu2nd  17928  resf2nd  17946  wunfunc  17952  wunfuncOLD  17953  homaval  18085  setcco  18137  catcco  18159  estrcco  18185  xpcco  18239  xpchom2  18242  xpcco2  18243  xpccatid  18244  prfcl  18259  prf1st  18260  prf2nd  18261  evlf2  18275  curf1cl  18285  curf2cl  18288  curfcl  18289  uncf1  18293  uncf2  18294  uncfcurf  18296  diag11  18300  diag12  18301  diag2  18302  curf2ndf  18304  hof2fval  18312  yonedalem21  18330  yonedalem22  18335  yonedalem3b  18336  yonffthlem  18339  latcl2  18494  xpsmnd0  18804  xpsinv  19091  xpsgrpsub  19092  lsmhash  19738  frgpuplem  19805  xpsring1d  20347  rngqiprngimf  21325  pzriprnglem4  21513  pzriprnglem5  21514  pzriprnglem8  21517  pzriprnglem12  21521  mdetrlin  22624  mdetrsca  22625  txcls  23628  txcnp  23644  txcnmpt  23648  txdis1cn  23659  txlly  23660  txnlly  23661  txlm  23672  lmcn2  23673  txkgen  23676  xkococnlem  23683  txhmeo  23827  ptuncnv  23831  txflf  24030  flfcnp2  24031  tmdcn2  24113  qustgplem  24145  tsmsadd  24171  imasdsf1olem  24399  xpsdsval  24407  comet  24542  metustid  24583  metustexhalf  24585  metuel2  24594  tngnm  24688  cnheiborlem  25000  bcthlem5  25376  ovollb2lem  25537  ovolctb  25539  ovoliunlem2  25552  ovolshftlem1  25558  ovolscalem1  25562  ovolicc1  25565  ioombl1lem1  25607  dyadf  25640  itg1addlem4  25748  itg1addlem4OLD  25749  limccnp2  25942  dvaddbr  25989  dvmulbr  25990  dvmulbrOLD  25991  dvcobr  25998  dvcobrOLD  25999  lhop1lem  26067  cxpcn3  26806  mpodvdsmulf1o  27252  dvdsmulf1o  27254  addsqnreup  27502  addsval  28010  mulsval  28150  tgjustc1  28498  tgjustc2  28499  tgelrnln  28653  numclwwlk1lem2f  30384  ofresid  32659  fsuppcurry1  32743  fsuppcurry2  32744  gsumpart  33043  gsumwrd2dccatlem  33052  gsumwrd2dccat  33053  erlbrd  33250  rlocaddval  33255  rlocmulval  33256  rloccring  33257  rloc0g  33258  rloc1r  33259  rlocf1  33260  fracerl  33288  fracfld  33290  zringfrac  33562  prsdm  33875  prsrn  33876  esum2dlem  34073  hgt750lemb  34650  cvmlift2lem10  35297  goelel3xp  35333  sat1el2xp  35364  fmla0xp  35368  prv1n  35416  pprodss4v  35866  poimirlem3  37610  poimirlem4  37611  poimirlem17  37624  poimirlem20  37627  mblfinlem2  37645  aks6d1c3  42105  aks6d1c7lem1  42162  f1o2d2  42253  projf1o  45140  ovolval4lem1  46605  ovolval5lem2  46609  gpgedgel  47943  gpgvtx0  47944  gpgvtx1  47945