Theorem opelxpd 5694

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ⟨cop 4838   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-xp 5661

This theorem is used by:  otel3xp  5701  opabssxpd  5702  relssdmrn  6286  fpr2g  7237  fliftrel  7336  elovimad  7490  el2xptp0  8068  oprab2co  8131  1stconst  8135  2ndconst  8136  curry2  8142  fsplitfpar  8153  offsplitfpar  8154  mpof1o2d  8161  fnwelem  8167  xpf1o  9183  xpmapenlem  9188  unxpdomlem3  9274  fseqenlem1  10127  fseqenlem2  10128  iundom2g  10648  ordpipq  11051  addpqf  11053  mulpqf  11055  recmulnq  11073  ltexnq  11084  axmulf  11255  cnrecnv  15358  ruclem1  16425  eucalgf  16784  qredeu  16859  crth  16981  phimullem  16982  prmreclem3  17122  setsstruct2  17378  imasaddflem  17728  xpsaddlem  17771  xpsvsca  17775  xpsle  17777  comffval  17899  oppccofval  17916  isoval  17966  brcic  17999  funcf2  18069  idfu2nd  18078  resf2nd  18096  wunfunc  18102  homaval  18232  setcco  18284  catcco  18306  estrcco  18330  xpcco  18383  xpchom2  18386  xpcco2  18387  xpccatid  18388  prfcl  18403  prf1st  18404  prf2nd  18405  evlf2  18418  curf1cl  18428  curf2cl  18431  curfcl  18432  uncf1  18436  uncf2  18437  uncfcurf  18439  diag11  18443  diag12  18444  diag2  18445  curf2ndf  18447  hof2fval  18455  yonedalem21  18473  yonedalem22  18478  yonedalem3b  18479  yonffthlem  18482  latcl2  18636  xpsmnd0  18998  xpsinv  19296  xpsgrpsub  19297  lsmhash  19946  frgpuplem  20013  xpsring1d  20590  rngqiprngimf  21620  pzriprnglem4  21817  pzriprnglem5  21818  pzriprnglem8  21821  pzriprnglem12  21825  mdetrlin  22944  mdetrsca  22945  txcls  23950  txcnp  23966  txcnmpt  23970  txdis1cn  23981  txlly  23982  txnlly  23983  txlm  23994  lmcn2  23995  txkgen  23998  xkococnlem  24005  txhmeo  24149  ptuncnv  24153  txflf  24352  flfcnp2  24353  tmdcn2  24435  qustgplem  24467  tsmsadd  24493  imasdsf1olem  24719  xpsdsval  24727  comet  24859  metustid  24900  metustexhalf  24902  metuel2  24911  tngnm  24997  cnheiborlem  25302  bcthlem5  25676  ovollb2lem  25836  ovolctb  25838  ovoliunlem2  25851  ovolshftlem1  25857  ovolscalem1  25861  ovolicc1  25864  ioombl1lem1  25906  dyadf  25939  itg1addlem4  26047  limccnp2  26239  dvaddbr  26285  dvmulbr  26286  dvcobr  26293  lhop1lem  26360  cxpcn3  27103  mpodvdsmulf1o  27548  dvdsmulf1o  27550  addsqnreup  27797  addsval  28375  mulsval  28522  tgjustc1  28964  tgjustc2  28965  tgelrnln  29125  tgelrnpln  29281  numclwwlk1lem2f  30983  ofresid  33305  fsuppcurry1  33383  fsuppcurry2  33384  gsumpart  33691  gsumwrd2dccatlem  33705  gsumwrd2dccat  33706  elrgspnsubrunlem2  33876  erlbrd  33891  erld2  33894  rlocaddval  33897  rlocmulval  33898  rloccring  33899  rloc0g  33900  rloc1r  33901  rlocf1  33902  rlocinvunit  33903  rlocisunit  33904  fracerl  33935  fracfld  33937  zringfrac  34153  prsdm  34613  prsrn  34614  esum2dlem  34791  hgt750lemb  35352  mpofvopd  35795  brlexod  35998  brr0d  36000  maxssj0  36005  j0ltalephlem  36006  cvmlift2lem10  36243  goelel3xp  36279  sat1el2xp  36310  fmla0xp  36314  prv1n  36362  pprodss4v  36823  nmulprop  37116  poimirlem3  38732  poimirlem4  38733  poimirlem17  38746  poimirlem20  38749  mblfinlem2  38767  aks6d1c3  43364  aks6d1c7lem1  43421  projf1o  46414  hoicvr  47761  ovolval4lem1  47862  ovolval5lem2  47866  gpgiedgdmellem  49347  gpgvtx0  49354  gpgvtx1  49355  gpg3kgrtriex  49390  gpgprismgr4cycllem3  49398  gpgprismgr4cycllem9  49404  tposidres  50202  ixpovf  50400  oppf1st2nd  50450  imaid  50473  xpcfuccocl  50582  swapf1  50597  swapf2val  50598  swapf2  50599  cofuswapf1  50619  cofuswapf2  50620  fucoaltvallem  50695  parcoval  50965  lanfval  50999  ranfval  51000