Theorem op1std 7996

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 6875	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1st 7994	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
5	1, 4	eqtrdi 2786	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ⟨cop 4607  ‘cfv 6530  1^st c1st 7984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fv 6538  df-1st 7986

This theorem is referenced by:  1st2val  8014  xp1st  8018  sbcopeq1a  8046  csbopeq1a  8047  eloprabi  8060  mpomptsx  8061  dmmpossx  8063  fmpox  8064  ovmptss  8090  fmpoco  8092  df1st2  8095  fsplit  8114  frxp  8123  xporderlem  8124  fnwelem  8128  fimaproj  8132  xpord2lem  8139  naddcllem  8686  xpf1o  9151  mapunen  9158  xpwdomg  9597  hsmexlem2  10439  fsumcom2  15788  fprodcom2  15998  qredeu  16675  isfuncd  17876  cofucl  17899  funcres2b  17908  funcpropd  17913  xpcco1st  18194  xpccatid  18198  1stf1  18202  2ndf1  18205  1stfcl  18207  prf1  18210  prfcl  18213  prf1st  18214  prf2nd  18215  evlf1  18230  evlfcl  18232  curf1fval  18234  curf11  18236  curf1cl  18238  curfcl  18242  hof1fval  18263  txbas  23503  cnmpt1st  23604  txhmeo  23739  ptuncnv  23743  ptunhmeo  23744  xpstopnlem1  23745  xkohmeo  23751  prdstmdd  24060  ucnimalem  24216  fmucndlem  24227  fsum2cn  24811  ovoliunlem1  25453  lgsquadlem1  27341  lgsquadlem2  27342  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  clwlkclwwlkfolem  29934  wlkl0  30294  gsumhashmul  33001  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  elrgspnlem2  33184  elrgspnsubrunlem2  33189  eulerpartlemgs2  34358  hgt750lemb  34634  cvmliftlem15  35266  satfv1  35331  satfdmlem  35336  fmlasuc  35354  msubty  35495  msubco  35499  msubvrs  35528  filnetlem4  36345  finixpnum  37575  poimirlem4  37594  poimirlem15  37605  poimirlem20  37610  poimirlem26  37616  poimirlem28  37618  heicant  37625  dicelvalN  41143  aks6d1c2p1  42077  aks6d1c3  42082  aks6d1c4  42083  aks6d1c6lem2  42130  aks6d1c6lem4  42132  aks6d1c7lem1  42139  fmpocos  42232  rmxypairf1o  42882  unxpwdom3  43066  fgraphxp  43175  elcnvlem  43572  dvnprodlem2  45924  etransclem46  46257  ovnsubaddlem1  46547  gpgvtxedg0  48015  gpgvtxedg1  48016  gpgcubic  48029  gpg5nbgr3star  48031  dmmpossx2  48260  2arymaptf  48580  rrx2plordisom  48651  eloprab1st2nd  48791  funcf2lem  48994  tposcurf1  49158  reldmprcof1  49239  setc1ocofval  49327