Theorem op1std 8011

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ⟨cop 4590  ‘cfv 6538  1^st c1st 7999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001

This theorem is used by:  1st2val  8029  xp1st  8033  sbcopeq1a  8060  csbopeq1a  8061  eloprabi  8074  mpomptsx  8075  dmmpossx  8077  fmpox  8078  ovmptss  8104  fmpoco  8106  df1st2  8109  fsplit  8128  frxp  8138  xporderlem  8139  fnwelem  8143  fimaproj  8152  xpord2lem  8159  naddcllem  8685  xpf1o  9158  mapunen  9165  xpwdomg  9579  hsmexlem2  10505  fsumcom2  15940  fprodcom2  16151  qredeu  16833  isfuncd  18040  cofucl  18063  funcres2b  18072  funcpropd  18077  xpcco1st  18358  xpccatid  18362  1stf1  18366  2ndf1  18369  1stfcl  18371  prf1  18374  prfcl  18377  prf1st  18378  prf2nd  18379  evlf1  18394  evlfcl  18396  curf1fval  18398  curf11  18400  curf1cl  18402  curfcl  18406  hof1fval  18427  txbas  23886  cnmpt1st  23987  txhmeo  24122  ptuncnv  24126  ptunhmeo  24127  xpstopnlem1  24128  xkohmeo  24134  prdstmdd  24443  ucnimalem  24598  fmucndlem  24609  fsum2cn  25192  ovoliunlem1  25823  lgsquadlem1  27707  lgsquadlem2  27708  2sqreuop  27789  2sqreuopnn  27790  2sqreuoplt  27791  2sqreuopltb  27792  2sqreuopnnlt  27793  2sqreuopnnltb  27794  clwlkclwwlkfolem  30598  wlkl0  30968  gsumhashmul  33628  gsumwrd2dccatlem  33638  gsumwrd2dccat  33639  conjga  33731  elrgspnlem2  33804  elrgspnsubrunlem2  33809  mplvrpmga  34177  eulerpartlemgs2  35012  hgt750lemb  35285  cvmliftlem15  36063  satfv1  36128  satfdmlem  36133  fmlasuc  36151  msubty  36292  msubco  36296  msubvrs  36325  nmulprop  36939  filnetlem4  37169  finixpnum  38528  poimirlem4  38542  poimirlem15  38553  poimirlem20  38558  poimirlem26  38564  poimirlem28  38566  heicant  38573  dicelvalN  42235  aks6d1c2p1  43168  aks6d1c3  43173  aks6d1c4  43174  aks6d1c6lem2  43221  aks6d1c6lem4  43223  aks6d1c7lem1  43230  fmpocos  43287  rmxypairf1o  43917  unxpwdom3  44096  fgraphxp  44205  elcnvlem  44600  dvnprodlem2  46956  etransclem46  47289  ovnsubaddlem1  47579  gpgvtxedg0  49160  gpgvtxedg1  49161  gpgcubic  49176  gpg5nbgr3star  49178  pgnbgreunbgrlem3  49215  pgnbgreunbgrlem6  49221  dmmpossx2  49448  2arymaptf  49763  rrx2plordisom  49834  eloprab1st2nd  49977  funcf2lem  50188  oppf1  50246  tposcurf1  50406  reldmprcof1  50488  opf11  50510  setc1ocofval  50601