Theorem op1std 7981

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ⟨cop 4633  ‘cfv 6540  1^st c1st 7969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fv 6548  df-1st 7971

This theorem is referenced by:  1st2val  7999  xp1st  8003  sbcopeq1a  8031  csbopeq1a  8032  eloprabi  8045  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fmpoco  8077  df1st2  8080  fsplit  8099  frxp  8108  xporderlem  8109  fnwelem  8113  fimaproj  8117  xpord2lem  8124  naddcllem  8671  xpf1o  9135  mapunen  9142  xpwdomg  9576  hsmexlem2  10418  fsumcom2  15716  fprodcom2  15924  qredeu  16591  isfuncd  17811  cofucl  17834  funcres2b  17843  funcpropd  17847  xpcco1st  18132  xpccatid  18136  1stf1  18140  2ndf1  18143  1stfcl  18145  prf1  18148  prfcl  18151  prf1st  18152  prf2nd  18153  evlf1  18169  evlfcl  18171  curf1fval  18173  curf11  18175  curf1cl  18177  curfcl  18181  hof1fval  18202  txbas  23062  cnmpt1st  23163  txhmeo  23298  ptuncnv  23302  ptunhmeo  23303  xpstopnlem1  23304  xkohmeo  23310  prdstmdd  23619  ucnimalem  23776  fmucndlem  23787  fsum2cn  24378  ovoliunlem1  25010  lgsquadlem1  26872  lgsquadlem2  26873  2sqreuop  26954  2sqreuopnn  26955  2sqreuoplt  26956  2sqreuopltb  26957  2sqreuopnnlt  26958  2sqreuopnnltb  26959  clwlkclwwlkfolem  29249  wlkl0  29609  gsumhashmul  32195  eulerpartlemgs2  33367  hgt750lemb  33656  cvmliftlem15  34277  satfv1  34342  satfdmlem  34347  fmlasuc  34365  msubty  34506  msubco  34510  msubvrs  34539  filnetlem4  35254  finixpnum  36461  poimirlem4  36480  poimirlem15  36491  poimirlem20  36496  poimirlem26  36502  poimirlem28  36504  heicant  36511  dicelvalN  40037  aks6d1c2p1  40944  fmpocos  41053  rmxypairf1o  41635  unxpwdom3  41822  fgraphxp  41938  elcnvlem  42337  dvnprodlem2  44649  etransclem46  44982  ovnsubaddlem1  45272  dmmpossx2  46965  2arymaptf  47291  rrx2plordisom  47362  funcf2lem  47591