Theorem opelxpd 5699

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ⟨cop 4594   × cxp 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-opab 5173  df-xp 5666

This theorem is used by:  otel3xp  5706  opabssxpd  5707  relssdmrn  6270  fpr2g  7209  fliftrel  7306  elovimad  7462  el2xptp0  8031  oprab2co  8090  1stconst  8093  2ndconst  8094  curry2  8100  fsplitfpar  8111  offsplitfpar  8112  mpof1o2d  8119  fnwelem  8125  xpf1o  9125  xpmapenlem  9130  unxpdomlem3  9216  fseqenlem1  10015  fseqenlem2  10016  iundom2g  10530  ordpipq  10933  addpqf  10935  mulpqf  10937  recmulnq  10955  ltexnq  10966  axmulf  11137  cnrecnv  15223  ruclem1  16293  eucalgf  16647  qredeu  16722  crth  16843  phimullem  16844  prmreclem3  16984  setsstruct2  17240  imasaddflem  17590  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  comffval  17761  oppccofval  17778  isoval  17828  brcic  17861  funcf2  17931  idfu2nd  17940  resf2nd  17958  wunfunc  17964  homaval  18094  setcco  18146  catcco  18168  estrcco  18192  xpcco  18245  xpchom2  18248  xpcco2  18249  xpccatid  18250  prfcl  18265  prf1st  18266  prf2nd  18267  evlf2  18280  curf1cl  18290  curf2cl  18293  curfcl  18294  uncf1  18298  uncf2  18299  uncfcurf  18301  diag11  18305  diag12  18306  diag2  18307  curf2ndf  18309  hof2fval  18317  yonedalem21  18335  yonedalem22  18340  yonedalem3b  18341  yonffthlem  18344  latcl2  18498  xpsmnd0  18842  xpsinv  19132  xpsgrpsub  19133  lsmhash  19781  frgpuplem  19848  xpsring1d  20422  rngqiprngimf  21448  pzriprnglem4  21645  pzriprnglem5  21646  pzriprnglem8  21649  pzriprnglem12  21653  mdetrlin  22770  mdetrsca  22771  txcls  23772  txcnp  23788  txcnmpt  23792  txdis1cn  23803  txlly  23804  txnlly  23805  txlm  23816  lmcn2  23817  txkgen  23820  xkococnlem  23827  txhmeo  23971  ptuncnv  23975  txflf  24174  flfcnp2  24175  tmdcn2  24257  qustgplem  24289  tsmsadd  24315  imasdsf1olem  24541  xpsdsval  24549  comet  24681  metustid  24722  metustexhalf  24724  metuel2  24733  tngnm  24819  cnheiborlem  25124  bcthlem5  25498  ovollb2lem  25658  ovolctb  25660  ovoliunlem2  25673  ovolshftlem1  25679  ovolscalem1  25683  ovolicc1  25686  ioombl1lem1  25728  dyadf  25761  itg1addlem4  25869  limccnp2  26062  dvaddbr  26108  dvmulbr  26109  dvcobr  26116  lhop1lem  26183  cxpcn3  26924  mpodvdsmulf1o  27369  dvdsmulf1o  27371  addsqnreup  27618  addsval  28166  mulsval  28313  tgjustc1  28755  tgjustc2  28756  tgelrnln  28914  tgelrnpln  29069  numclwwlk1lem2f  30717  ofresid  32998  fsuppcurry1  33080  fsuppcurry2  33081  gsumpart  33392  gsumwrd2dccatlem  33406  gsumwrd2dccat  33407  elrgspnsubrunlem2  33577  erlbrd  33592  erld2  33595  rlocaddval  33598  rlocmulval  33599  rloccring  33600  rloc0g  33601  rloc1r  33602  rlocf1  33603  rlocinvunit  33604  rlocisunit  33605  fracerl  33636  fracfld  33638  zringfrac  33853  prsdm  34313  prsrn  34314  esum2dlem  34491  hgt750lemb  35052  cvmlift2lem10  35812  goelel3xp  35848  sat1el2xp  35879  fmla0xp  35883  prv1n  35931  pprodss4v  36382  nmulprop  36690  poimirlem3  38302  poimirlem4  38303  poimirlem17  38316  poimirlem20  38319  mblfinlem2  38337  aks6d1c3  42918  aks6d1c7lem1  42975  projf1o  45942  hoicvr  47290  ovolval4lem1  47391  ovolval5lem2  47395  gpgiedgdmellem  48839  gpgvtx0  48846  gpgvtx1  48847  gpg3kgrtriex  48882  gpgprismgr4cycllem3  48890  gpgprismgr4cycllem9  48896  tposidres  49692  oppf1st2nd  49937  imaid  49960  xpcfuccocl  50063  swapf1  50078  swapf2val  50079  swapf2  50080  cofuswapf1  50100  cofuswapf2  50101  lanfval  50419  ranfval  50420