Theorem op1std 7980

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  Vcvv 3454  ⟨cop 4588  ‘cfv 6521  1^st c1st 7968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6477  df-fun 6523  df-fv 6529  df-1st 7970

This theorem is referenced by:  1st2val  7998  xp1st  8002  sbcopeq1a  8030  csbopeq1a  8031  eloprabi  8044  mpomptsx  8045  dmmpossx  8047  fmpox  8048  ovmptss  8072  fmpoco  8074  df1st2  8077  fsplit  8096  frxp  8106  xporderlem  8107  fnwelem  8111  fimaproj  8115  xpord2lem  8122  naddcllem  8646  xpf1o  9111  mapunen  9118  xpwdomg  9533  hsmexlem2  10384  fsumcom2  15801  fprodcom2  16014  qredeu  16692  isfuncd  17898  cofucl  17921  funcres2b  17930  funcpropd  17935  xpcco1st  18216  xpccatid  18220  1stf1  18224  2ndf1  18227  1stfcl  18229  prf1  18232  prfcl  18235  prf1st  18236  prf2nd  18237  evlf1  18252  evlfcl  18254  curf1fval  18256  curf11  18258  curf1cl  18260  curfcl  18264  hof1fval  18285  txbas  23624  cnmpt1st  23725  txhmeo  23860  ptuncnv  23864  ptunhmeo  23865  xpstopnlem1  23866  xkohmeo  23872  prdstmdd  24181  ucnimalem  24336  fmucndlem  24347  fsum2cn  24930  ovoliunlem1  25561  lgsquadlem1  27441  lgsquadlem2  27442  2sqreuop  27523  2sqreuopnn  27524  2sqreuoplt  27525  2sqreuopltb  27526  2sqreuopnnlt  27527  2sqreuopnnltb  27528  clwlkclwwlkfolem  30206  wlkl0  30566  gsumhashmul  33244  gsumwrd2dccatlem  33254  gsumwrd2dccat  33255  conjga  33347  elrgspnlem2  33421  elrgspnsubrunlem2  33426  mplvrpmga  33839  eulerpartlemgs2  34674  hgt750lemb  34947  cvmliftlem15  35645  satfv1  35710  satfdmlem  35715  fmlasuc  35733  msubty  35874  msubco  35878  msubvrs  35907  nmulprop  36537  filnetlem4  36738  finixpnum  38101  poimirlem4  38120  poimirlem15  38131  poimirlem20  38136  poimirlem26  38142  poimirlem28  38144  heicant  38151  dicelvalN  41799  aks6d1c2p1  42732  aks6d1c3  42737  aks6d1c4  42738  aks6d1c6lem2  42785  aks6d1c6lem4  42787  aks6d1c7lem1  42794  fmpocos  42849  rmxypairf1o  43485  unxpwdom3  43669  fgraphxp  43778  elcnvlem  44174  dvnprodlem2  46518  etransclem46  46851  ovnsubaddlem1  47141  gpgvtxedg0  48682  gpgvtxedg1  48683  gpgcubic  48698  gpg5nbgr3star  48700  pgnbgreunbgrlem3  48737  pgnbgreunbgrlem6  48743  dmmpossx2  48956  2arymaptf  49271  rrx2plordisom  49342  eloprab1st2nd  49486  funcf2lem  49699  oppf1  49757  tposcurf1  49917  reldmprcof1  49999  opf11  50021  setc1ocofval  50112