Theorem op1std 8022

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ⟨cop 4636  ‘cfv 6562  1^st c1st 8010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fv 6570  df-1st 8012

This theorem is referenced by:  1st2val  8040  xp1st  8044  sbcopeq1a  8072  csbopeq1a  8073  eloprabi  8086  mpomptsx  8087  dmmpossx  8089  fmpox  8090  ovmptss  8116  fmpoco  8118  df1st2  8121  fsplit  8140  frxp  8149  xporderlem  8150  fnwelem  8154  fimaproj  8158  xpord2lem  8165  naddcllem  8712  xpf1o  9177  mapunen  9184  xpwdomg  9622  hsmexlem2  10464  fsumcom2  15806  fprodcom2  16016  qredeu  16691  isfuncd  17915  cofucl  17938  funcres2b  17947  funcpropd  17953  xpcco1st  18239  xpccatid  18243  1stf1  18247  2ndf1  18250  1stfcl  18252  prf1  18255  prfcl  18258  prf1st  18259  prf2nd  18260  evlf1  18276  evlfcl  18278  curf1fval  18280  curf11  18282  curf1cl  18284  curfcl  18288  hof1fval  18309  txbas  23590  cnmpt1st  23691  txhmeo  23826  ptuncnv  23830  ptunhmeo  23831  xpstopnlem1  23832  xkohmeo  23838  prdstmdd  24147  ucnimalem  24304  fmucndlem  24315  fsum2cn  24908  ovoliunlem1  25550  lgsquadlem1  27438  lgsquadlem2  27439  2sqreuop  27520  2sqreuopnn  27521  2sqreuoplt  27522  2sqreuopltb  27523  2sqreuopnnlt  27524  2sqreuopnnltb  27525  clwlkclwwlkfolem  30035  wlkl0  30395  gsumhashmul  33046  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  elrgspnlem2  33232  eulerpartlemgs2  34361  hgt750lemb  34649  cvmliftlem15  35282  satfv1  35347  satfdmlem  35352  fmlasuc  35370  msubty  35511  msubco  35515  msubvrs  35544  filnetlem4  36363  finixpnum  37591  poimirlem4  37610  poimirlem15  37621  poimirlem20  37626  poimirlem26  37632  poimirlem28  37634  heicant  37641  dicelvalN  41160  aks6d1c2p1  42099  aks6d1c3  42104  aks6d1c4  42105  aks6d1c6lem2  42152  aks6d1c6lem4  42154  aks6d1c7lem1  42161  fmpocos  42253  rmxypairf1o  42899  unxpwdom3  43083  fgraphxp  43192  elcnvlem  43590  dvnprodlem2  45902  etransclem46  46235  ovnsubaddlem1  46525  gpgvtxedg0  47955  gpgvtxedg1  47956  gpgcubic  47969  gpg5nbgr3star  47971  dmmpossx2  48181  2arymaptf  48501  rrx2plordisom  48572  funcf2lem  48810