Theorem opelxpd 5715

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

Syntax hints:   → wi 4   ∈ wcel 2106  ⟨cop 4634   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-xp 5682

This theorem is referenced by:  otel3xp  5722  opabssxpd  5723  relssdmrn  6267  fpr2g  7212  fliftrel  7304  elovimad  7456  el2xptp0  8021  oprab2co  8082  1stconst  8085  2ndconst  8086  curry2  8092  fsplitfpar  8103  offsplitfpar  8104  fnwelem  8116  xpf1o  9138  xpmapenlem  9143  unxpdomlem3  9251  fseqenlem1  10018  fseqenlem2  10019  iundom2g  10534  ordpipq  10936  addpqf  10938  mulpqf  10940  recmulnq  10958  ltexnq  10969  axmulf  11140  cnrecnv  15111  ruclem1  16173  eucalgf  16519  qredeu  16594  crth  16710  phimullem  16711  prmreclem3  16850  setsstruct2  17106  imasaddflem  17475  xpsaddlem  17518  xpsvsca  17522  xpsle  17524  comffval  17642  oppccofval  17660  isoval  17711  brcic  17744  funcf2  17817  idfu2nd  17826  resf2nd  17844  wunfunc  17848  wunfuncOLD  17849  homaval  17980  setcco  18032  catcco  18054  estrcco  18080  xpcco  18134  xpchom2  18137  xpcco2  18138  xpccatid  18139  prfcl  18154  prf1st  18155  prf2nd  18156  evlf2  18170  curf1cl  18180  curf2cl  18183  curfcl  18184  uncf1  18188  uncf2  18189  uncfcurf  18191  diag11  18195  diag12  18196  diag2  18197  curf2ndf  18199  hof2fval  18207  yonedalem21  18225  yonedalem22  18230  yonedalem3b  18231  yonffthlem  18234  latcl2  18388  xpsmnd0  18665  xpsinv  18942  xpsgrpsub  18943  lsmhash  19572  frgpuplem  19639  xpsring1d  20145  mdetrlin  22103  mdetrsca  22104  txcls  23107  txcnp  23123  txcnmpt  23127  txdis1cn  23138  txlly  23139  txnlly  23140  txlm  23151  lmcn2  23152  txkgen  23155  xkococnlem  23162  txhmeo  23306  ptuncnv  23310  txflf  23509  flfcnp2  23510  tmdcn2  23592  qustgplem  23624  tsmsadd  23650  imasdsf1olem  23878  xpsdsval  23886  comet  24021  metustid  24062  metustexhalf  24064  metuel2  24073  tngnm  24167  cnheiborlem  24469  bcthlem5  24844  ovollb2lem  25004  ovolctb  25006  ovoliunlem2  25019  ovolshftlem1  25025  ovolscalem1  25029  ovolicc1  25032  ioombl1lem1  25074  dyadf  25107  itg1addlem4  25215  itg1addlem4OLD  25216  limccnp2  25408  dvaddbr  25454  dvmulbr  25455  dvcobr  25462  lhop1lem  25529  cxpcn3  26253  dvdsmulf1o  26695  addsqnreup  26943  addsval  27443  mulsval  27562  tgjustc1  27723  tgjustc2  27724  tgelrnln  27878  numclwwlk1lem2f  29605  ofresid  31862  fsuppcurry1  31945  fsuppcurry2  31946  gsumpart  32202  prsdm  32889  prsrn  32890  esum2dlem  33085  hgt750lemb  33663  cvmlift2lem10  34298  goelel3xp  34334  sat1el2xp  34365  fmla0xp  34369  prv1n  34417  pprodss4v  34851  gg-dvmulbr  35170  gg-dvcobr  35171  poimirlem3  36486  poimirlem4  36487  poimirlem17  36500  poimirlem20  36503  mblfinlem2  36521  f1o2d2  41057  projf1o  43886  ovolval4lem1  45355  ovolval5lem2  45359  rngqiprngimf  46772  pzriprnglem4  46798  pzriprnglem5  46799  pzriprnglem8  46802  pzriprnglem12  46806