Theorem op1std 7992

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ⟨cop 4595  ‘cfv 6536  1^st c1st 7980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-1st 7982

This theorem is referenced by:  1st2val  8010  xp1st  8014  sbcopeq1a  8042  csbopeq1a  8043  eloprabi  8056  mpomptsx  8057  dmmpossx  8059  fmpox  8060  ovmptss  8084  fmpoco  8086  df1st2  8089  fsplit  8108  frxp  8118  xporderlem  8119  fnwelem  8123  fimaproj  8127  xpord2lem  8134  naddcllem  8658  xpf1o  9123  mapunen  9130  xpwdomg  9543  hsmexlem2  10406  fsumcom2  15821  fprodcom2  16034  qredeu  16711  isfuncd  17917  cofucl  17940  funcres2b  17949  funcpropd  17954  xpcco1st  18235  xpccatid  18239  1stf1  18243  2ndf1  18246  1stfcl  18248  prf1  18251  prfcl  18254  prf1st  18255  prf2nd  18256  evlf1  18271  evlfcl  18273  curf1fval  18275  curf11  18277  curf1cl  18279  curfcl  18283  hof1fval  18304  txbas  23724  cnmpt1st  23825  txhmeo  23960  ptuncnv  23964  ptunhmeo  23965  xpstopnlem1  23966  xkohmeo  23972  prdstmdd  24281  ucnimalem  24436  fmucndlem  24447  fsum2cn  25030  ovoliunlem1  25661  lgsquadlem1  27544  lgsquadlem2  27545  2sqreuop  27626  2sqreuopnn  27627  2sqreuoplt  27628  2sqreuopltb  27629  2sqreuopnnlt  27630  2sqreuopnnltb  27631  clwlkclwwlkfolem  30358  wlkl0  30718  gsumhashmul  33387  gsumwrd2dccatlem  33397  gsumwrd2dccat  33398  conjga  33490  elrgspnlem2  33563  elrgspnsubrunlem2  33568  mplvrpmga  33935  eulerpartlemgs2  34770  hgt750lemb  35043  cvmliftlem15  35790  satfv1  35855  satfdmlem  35860  fmlasuc  35878  msubty  36019  msubco  36023  msubvrs  36052  nmulprop  36682  filnetlem4  36892  finixpnum  38256  poimirlem4  38275  poimirlem15  38286  poimirlem20  38291  poimirlem26  38297  poimirlem28  38299  heicant  38306  dicelvalN  41952  aks6d1c2p1  42885  aks6d1c3  42890  aks6d1c4  42891  aks6d1c6lem2  42938  aks6d1c6lem4  42940  aks6d1c7lem1  42947  fmpocos  43004  rmxypairf1o  43638  unxpwdom3  43822  fgraphxp  43931  elcnvlem  44327  dvnprodlem2  46661  etransclem46  46994  ovnsubaddlem1  47284  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgcubic  48844  gpg5nbgr3star  48846  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889  dmmpossx2  49117  2arymaptf  49432  rrx2plordisom  49503  eloprab1st2nd  49646  funcf2lem  49859  oppf1  49917  tposcurf1  50077  reldmprcof1  50159  opf11  50181  setc1ocofval  50272