Theorem op1std 7946

Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
op1st.1	⊢ 𝐴 ∈ V
op1st.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
op1std	⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)

Proof of Theorem op1std

Step	Hyp	Ref	Expression
1		fveq2 6835	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1st 7944	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
5	1, 4	eqtrdi 2788	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574  ‘cfv 6493  1^st c1st 7934

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-1st 7936

This theorem is referenced by:  1st2val  7964  xp1st  7968  sbcopeq1a  7996  csbopeq1a  7997  eloprabi  8010  mpomptsx  8011  dmmpossx  8013  fmpox  8014  ovmptss  8037  fmpoco  8039  df1st2  8042  fsplit  8061  frxp  8070  xporderlem  8071  fnwelem  8075  fimaproj  8079  xpord2lem  8086  naddcllem  8606  xpf1o  9071  mapunen  9078  xpwdomg  9494  hsmexlem2  10343  fsumcom2  15730  fprodcom2  15943  qredeu  16621  isfuncd  17826  cofucl  17849  funcres2b  17858  funcpropd  17863  xpcco1st  18144  xpccatid  18148  1stf1  18152  2ndf1  18155  1stfcl  18157  prf1  18160  prfcl  18163  prf1st  18164  prf2nd  18165  evlf1  18180  evlfcl  18182  curf1fval  18184  curf11  18186  curf1cl  18188  curfcl  18192  hof1fval  18213  txbas  23545  cnmpt1st  23646  txhmeo  23781  ptuncnv  23785  ptunhmeo  23786  xpstopnlem1  23787  xkohmeo  23793  prdstmdd  24102  ucnimalem  24257  fmucndlem  24268  fsum2cn  24851  ovoliunlem1  25482  lgsquadlem1  27360  lgsquadlem2  27361  2sqreuop  27442  2sqreuopnn  27443  2sqreuoplt  27444  2sqreuopltb  27445  2sqreuopnnlt  27446  2sqreuopnnltb  27447  clwlkclwwlkfolem  30095  wlkl0  30455  gsumhashmul  33146  gsumwrd2dccatlem  33156  gsumwrd2dccat  33157  conjga  33249  elrgspnlem2  33322  elrgspnsubrunlem2  33327  mplvrpmga  33707  eulerpartlemgs2  34543  hgt750lemb  34819  cvmliftlem15  35499  satfv1  35564  satfdmlem  35569  fmlasuc  35587  msubty  35728  msubco  35732  msubvrs  35761  filnetlem4  36582  finixpnum  37943  poimirlem4  37962  poimirlem15  37973  poimirlem20  37978  poimirlem26  37984  poimirlem28  37986  heicant  37993  dicelvalN  41641  aks6d1c2p1  42574  aks6d1c3  42579  aks6d1c4  42580  aks6d1c6lem2  42627  aks6d1c6lem4  42629  aks6d1c7lem1  42636  fmpocos  42692  rmxypairf1o  43360  unxpwdom3  43544  fgraphxp  43653  elcnvlem  44049  dvnprodlem2  46396  etransclem46  46729  ovnsubaddlem1  47019  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgcubic  48570  gpg5nbgr3star  48572  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  dmmpossx2  48828  2arymaptf  49143  rrx2plordisom  49214  eloprab1st2nd  49358  funcf2lem  49571  oppf1  49629  tposcurf1  49789  reldmprcof1  49871  opf11  49893  setc1ocofval  49984