Theorem opelxpd 5698

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ⟨cop 4593   × cxp 5657

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-xp 5665

This theorem is used by:  otel3xp  5705  opabssxpd  5706  relssdmrn  6270  fpr2g  7213  fliftrel  7312  elovimad  7466  el2xptp0  8036  oprab2co  8097  1stconst  8100  2ndconst  8101  curry2  8107  fsplitfpar  8118  offsplitfpar  8119  mpof1o2d  8126  fnwelem  8132  xpf1o  9140  xpmapenlem  9145  unxpdomlem3  9231  fseqenlem1  10030  fseqenlem2  10031  iundom2g  10551  ordpipq  10954  addpqf  10956  mulpqf  10958  recmulnq  10976  ltexnq  10987  axmulf  11158  cnrecnv  15254  ruclem1  16323  eucalgf  16677  qredeu  16752  crth  16873  phimullem  16874  prmreclem3  17014  setsstruct2  17270  imasaddflem  17620  xpsaddlem  17663  xpsvsca  17667  xpsle  17669  comffval  17791  oppccofval  17808  isoval  17858  brcic  17891  funcf2  17961  idfu2nd  17970  resf2nd  17988  wunfunc  17994  homaval  18124  setcco  18176  catcco  18198  estrcco  18222  xpcco  18275  xpchom2  18278  xpcco2  18279  xpccatid  18280  prfcl  18295  prf1st  18296  prf2nd  18297  evlf2  18310  curf1cl  18320  curf2cl  18323  curfcl  18324  uncf1  18328  uncf2  18329  uncfcurf  18331  diag11  18335  diag12  18336  diag2  18337  curf2ndf  18339  hof2fval  18347  yonedalem21  18365  yonedalem22  18370  yonedalem3b  18371  yonffthlem  18374  latcl2  18528  xpsmnd0  18887  xpsinv  19184  xpsgrpsub  19185  lsmhash  19833  frgpuplem  19900  xpsring1d  20475  rngqiprngimf  21501  pzriprnglem4  21698  pzriprnglem5  21699  pzriprnglem8  21702  pzriprnglem12  21706  mdetrlin  22825  mdetrsca  22826  txcls  23831  txcnp  23847  txcnmpt  23851  txdis1cn  23862  txlly  23863  txnlly  23864  txlm  23875  lmcn2  23876  txkgen  23879  xkococnlem  23886  txhmeo  24030  ptuncnv  24034  txflf  24233  flfcnp2  24234  tmdcn2  24316  qustgplem  24348  tsmsadd  24374  imasdsf1olem  24600  xpsdsval  24608  comet  24740  metustid  24781  metustexhalf  24783  metuel2  24792  tngnm  24878  cnheiborlem  25183  bcthlem5  25557  ovollb2lem  25717  ovolctb  25719  ovoliunlem2  25732  ovolshftlem1  25738  ovolscalem1  25742  ovolicc1  25745  ioombl1lem1  25787  dyadf  25820  itg1addlem4  25928  limccnp2  26121  dvaddbr  26167  dvmulbr  26168  dvcobr  26175  lhop1lem  26242  cxpcn3  26983  mpodvdsmulf1o  27428  dvdsmulf1o  27430  addsqnreup  27677  addsval  28225  mulsval  28372  tgjustc1  28814  tgjustc2  28815  tgelrnln  28975  tgelrnpln  29131  numclwwlk1lem2f  30821  ofresid  33102  fsuppcurry1  33182  fsuppcurry2  33183  gsumpart  33490  gsumwrd2dccatlem  33504  gsumwrd2dccat  33505  elrgspnsubrunlem2  33675  erlbrd  33690  erld2  33693  rlocaddval  33696  rlocmulval  33697  rloccring  33698  rloc0g  33699  rloc1r  33700  rlocf1  33701  rlocinvunit  33702  rlocisunit  33703  fracerl  33734  fracfld  33736  zringfrac  33951  prsdm  34411  prsrn  34412  esum2dlem  34589  hgt750lemb  35151  cvmlift2lem10  35878  goelel3xp  35914  sat1el2xp  35945  fmla0xp  35949  prv1n  35997  pprodss4v  36448  nmulprop  36757  poimirlem3  38359  poimirlem4  38360  poimirlem17  38373  poimirlem20  38376  mblfinlem2  38394  aks6d1c3  42976  aks6d1c7lem1  43033  projf1o  46015  hoicvr  47363  ovolval4lem1  47464  ovolval5lem2  47468  gpgiedgdmellem  48949  gpgvtx0  48956  gpgvtx1  48957  gpg3kgrtriex  48992  gpgprismgr4cycllem3  49000  gpgprismgr4cycllem9  49006  tposidres  49799  oppf1st2nd  50044  imaid  50067  xpcfuccocl  50170  swapf1  50185  swapf2val  50186  swapf2  50187  cofuswapf1  50207  cofuswapf2  50208  lanfval  50526  ranfval  50527