Theorem op1std 7727

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3399  ⟨cop 4523  ‘cfv 6340  1^st c1st 7715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297  ax-un 7482

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3401  df-sbc 3682  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-iota 6298  df-fun 6342  df-fv 6348  df-1st 7717

This theorem is referenced by:  1st2val  7745  xp1st  7749  sbcopeq1a  7776  csbopeq1a  7777  eloprabi  7789  mpomptsx  7790  dmmpossx  7792  fmpox  7793  ovmptss  7817  fmpoco  7819  df1st2  7822  fsplit  7841  fsplitOLD  7842  frxp  7849  xporderlem  7850  fnwelem  7854  fimaproj  7858  xpf1o  8732  mapunen  8739  xpwdomg  9125  hsmexlem2  9930  fsumcom2  15225  fprodcom2  15433  qredeu  16102  isfuncd  17243  cofucl  17266  funcres2b  17275  funcpropd  17278  xpcco1st  17553  xpccatid  17557  1stf1  17561  2ndf1  17564  1stfcl  17566  prf1  17569  prfcl  17572  prf1st  17573  prf2nd  17574  evlf1  17589  evlfcl  17591  curf1fval  17593  curf11  17595  curf1cl  17597  curfcl  17601  hof1fval  17622  txbas  22321  cnmpt1st  22422  txhmeo  22557  ptuncnv  22561  ptunhmeo  22562  xpstopnlem1  22563  xkohmeo  22569  prdstmdd  22878  ucnimalem  23035  fmucndlem  23046  fsum2cn  23626  ovoliunlem1  24257  lgsquadlem1  26119  lgsquadlem2  26120  2sqreuop  26201  2sqreuopnn  26202  2sqreuoplt  26203  2sqreuopltb  26204  2sqreuopnnlt  26205  2sqreuopnnltb  26206  clwlkclwwlkfolem  27947  wlkl0  28307  gsumhashmul  30896  eulerpartlemgs2  31920  hgt750lemb  32209  cvmliftlem15  32834  satfv1  32899  satfdmlem  32904  fmlasuc  32922  msubty  33063  msubco  33067  msubvrs  33096  ot21std  33257  ot22ndd  33258  xpord2lem  33405  naddcllem  33477  filnetlem4  34216  finixpnum  35408  poimirlem4  35427  poimirlem15  35438  poimirlem20  35443  poimirlem26  35449  poimirlem28  35451  heicant  35458  dicelvalN  38838  rmxypairf1o  40328  unxpwdom3  40515  fgraphxp  40631  elcnvlem  40777  dvnprodlem2  43053  etransclem46  43386  ovnsubaddlem1  43673  dmmpossx2  45236  2arymaptf  45562  rrx2plordisom  45633