Theorem opelxpd 5704

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

Syntax hints:   → wi 4   ∈ wcel 2150  ⟨cop 4600   × cxp 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-sep 5262  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-xp 5671

This theorem is referenced by:  otel3xp  5711  opabssxpd  5712  relssdmrn  6274  fpr2g  7213  fliftrel  7310  elovimad  7464  el2xptp0  8036  oprab2co  8095  1stconst  8098  2ndconst  8099  curry2  8105  fsplitfpar  8116  offsplitfpar  8117  mpof1o2d  8124  fnwelem  8130  xpf1o  9130  xpmapenlem  9135  unxpdomlem3  9221  fseqenlem1  10011  fseqenlem2  10012  iundom2g  10527  ordpipq  10930  addpqf  10932  mulpqf  10934  recmulnq  10952  ltexnq  10963  axmulf  11134  cnrecnv  15219  ruclem1  16290  eucalgf  16644  qredeu  16719  crth  16840  phimullem  16841  prmreclem3  16981  setsstruct2  17237  imasaddflem  17587  xpsaddlem  17630  xpsvsca  17634  xpsle  17636  comffval  17758  oppccofval  17775  isoval  17825  brcic  17858  funcf2  17928  idfu2nd  17937  resf2nd  17955  wunfunc  17961  homaval  18091  setcco  18143  catcco  18165  estrcco  18189  xpcco  18242  xpchom2  18245  xpcco2  18246  xpccatid  18247  prfcl  18262  prf1st  18263  prf2nd  18264  evlf2  18277  curf1cl  18287  curf2cl  18290  curfcl  18291  uncf1  18295  uncf2  18296  uncfcurf  18298  diag11  18302  diag12  18303  diag2  18304  curf2ndf  18306  hof2fval  18314  yonedalem21  18332  yonedalem22  18337  yonedalem3b  18338  yonffthlem  18341  latcl2  18495  xpsmnd0  18839  xpsinv  19129  xpsgrpsub  19130  lsmhash  19778  frgpuplem  19845  xpsring1d  20418  rngqiprngimf  21420  pzriprnglem4  21617  pzriprnglem5  21618  pzriprnglem8  21621  pzriprnglem12  21625  mdetrlin  22742  mdetrsca  22743  txcls  23744  txcnp  23760  txcnmpt  23764  txdis1cn  23775  txlly  23776  txnlly  23777  txlm  23788  lmcn2  23789  txkgen  23792  xkococnlem  23799  txhmeo  23943  ptuncnv  23947  txflf  24146  flfcnp2  24147  tmdcn2  24229  qustgplem  24261  tsmsadd  24287  imasdsf1olem  24513  xpsdsval  24521  comet  24653  metustid  24694  metustexhalf  24696  metuel2  24705  tngnm  24791  cnheiborlem  25096  bcthlem5  25470  ovollb2lem  25630  ovolctb  25632  ovoliunlem2  25645  ovolshftlem1  25651  ovolscalem1  25655  ovolicc1  25658  ioombl1lem1  25700  dyadf  25733  itg1addlem4  25841  limccnp2  26034  dvaddbr  26080  dvmulbr  26081  dvcobr  26088  lhop1lem  26155  cxpcn3  26893  mpodvdsmulf1o  27338  dvdsmulf1o  27340  addsqnreup  27587  addsval  28135  mulsval  28282  tgjustc1  28724  tgjustc2  28725  tgelrnln  28883  tgelrnpln  29036  numclwwlk1lem2f  30676  ofresid  32957  fsuppcurry1  33039  fsuppcurry2  33040  gsumpart  33353  gsumwrd2dccatlem  33367  gsumwrd2dccat  33368  elrgspnsubrunlem2  33538  erlbrd  33553  erld2  33556  rlocaddval  33559  rlocmulval  33560  rloccring  33561  rloc0g  33562  rloc1r  33563  rlocf1  33564  rlocinvunit  33565  rlocisunit  33566  fracerl  33597  fracfld  33599  zringfrac  33814  prsdm  34274  prsrn  34275  esum2dlem  34452  hgt750lemb  35013  cvmlift2lem10  35762  goelel3xp  35798  sat1el2xp  35829  fmla0xp  35833  prv1n  35881  pprodss4v  36332  nmulprop  36640  poimirlem3  38222  poimirlem4  38223  poimirlem17  38236  poimirlem20  38239  mblfinlem2  38257  aks6d1c3  42840  aks6d1c7lem1  42897  projf1o  45866  hoicvr  47214  ovolval4lem1  47315  ovolval5lem2  47319  gpgiedgdmellem  48760  gpgvtx0  48767  gpgvtx1  48768  gpg3kgrtriex  48803  gpgprismgr4cycllem3  48811  gpgprismgr4cycllem9  48817  tposidres  49613  oppf1st2nd  49858  imaid  49881  xpcfuccocl  49984  swapf1  49999  swapf2val  50000  swapf2  50001  cofuswapf1  50021  cofuswapf2  50022  lanfval  50340  ranfval  50341