Theorem op1std 8015

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ⟨cop 4834  ‘cfv 6543  1^st c1st 8003

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6497  df-fun 6545  df-fv 6551  df-1st 8005

This theorem is used by:  1st2val  8033  xp1st  8037  sbcopeq1a  8064  csbopeq1a  8065  eloprabi  8078  mpomptsx  8079  dmmpossx  8081  fmpox  8082  ovmptssOLD  8109  fmpoco  8111  df1st2  8115  fsplit  8134  frxp  8144  xporderlem  8145  fnwelem  8149  fimaproj  8158  xpord2lem  8165  naddcllem  8692  xpf1o  9165  mapunen  9172  xpwdomg  9586  hsmexlem2  10512  fsumcom2  15949  fprodcom2  16160  qredeu  16842  isfuncd  18049  cofucl  18072  funcres2b  18081  funcpropd  18086  xpcco1st  18367  xpccatid  18371  1stf1  18375  2ndf1  18378  1stfcl  18380  prf1  18383  prfcl  18386  prf1st  18387  prf2nd  18388  evlf1  18403  evlfcl  18405  curf1fval  18407  curf11  18409  curf1cl  18411  curfcl  18415  hof1fval  18436  txbas  23895  cnmpt1st  23996  txhmeo  24131  ptuncnv  24135  ptunhmeo  24136  xpstopnlem1  24137  xkohmeo  24143  prdstmdd  24452  ucnimalem  24607  fmucndlem  24618  fsum2cn  25201  ovoliunlem1  25832  lgsquadlem1  27716  lgsquadlem2  27717  2sqreuop  27798  2sqreuopnn  27799  2sqreuoplt  27800  2sqreuopltb  27801  2sqreuopnnlt  27802  2sqreuopnnltb  27803  clwlkclwwlkfolem  30607  wlkl0  30977  gsumhashmul  33678  gsumwrd2dccatlem  33688  gsumwrd2dccat  33689  conjga  33781  elrgspnlem2  33854  elrgspnsubrunlem2  33859  mplvrpmga  34227  eulerpartlemgs2  35062  hgt750lemb  35335  cvmliftlem15  36153  satfv1  36218  satfdmlem  36223  fmlasuc  36241  msubty  36382  msubco  36386  msubvrs  36415  nmulprop  37035  filnetlem4  37265  finixpnum  38637  poimirlem4  38651  poimirlem15  38662  poimirlem20  38667  poimirlem26  38673  poimirlem28  38675  heicant  38682  dicelvalN  42344  aks6d1c2p1  43277  aks6d1c3  43282  aks6d1c4  43283  aks6d1c6lem2  43330  aks6d1c6lem4  43332  aks6d1c7lem1  43339  fmpocos  43396  rmxypairf1o  44027  unxpwdom3  44206  fgraphxp  44315  elcnvlem  44710  dvnprodlem2  47065  etransclem46  47398  ovnsubaddlem1  47688  gpgvtxedg0  49269  gpgvtxedg1  49270  gpgcubic  49285  gpg5nbgr3star  49287  pgnbgreunbgrlem3  49324  pgnbgreunbgrlem6  49330  dmmpossx2  49557  2arymaptf  49872  rrx2plordisom  49944  eloprab1st2nd  50087  funcf2lem  50303  oppf1  50363  tposcurf1  50529  postcof1st  50606  reldmprcof1  50624  opf11  50646  setc1ocofval  50737  fuconuniqlem  50889  fuconuniqvalslem  50891