Theorem op1std 7995

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ⟨cop 4600  ‘cfv 6537  1^st c1st 7983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7985

This theorem is referenced by:  1st2val  8013  xp1st  8017  sbcopeq1a  8045  csbopeq1a  8046  eloprabi  8059  mpomptsx  8060  dmmpossx  8062  fmpox  8063  ovmptss  8087  fmpoco  8089  df1st2  8092  fsplit  8111  frxp  8121  xporderlem  8122  fnwelem  8126  fimaproj  8130  xpord2lem  8137  naddcllem  8661  xpf1o  9126  mapunen  9133  xpwdomg  9546  hsmexlem2  10410  fsumcom2  15824  fprodcom2  16037  qredeu  16715  isfuncd  17921  cofucl  17944  funcres2b  17953  funcpropd  17958  xpcco1st  18239  xpccatid  18243  1stf1  18247  2ndf1  18250  1stfcl  18252  prf1  18255  prfcl  18258  prf1st  18259  prf2nd  18260  evlf1  18275  evlfcl  18277  curf1fval  18279  curf11  18281  curf1cl  18283  curfcl  18287  hof1fval  18308  txbas  23692  cnmpt1st  23793  txhmeo  23928  ptuncnv  23932  ptunhmeo  23933  xpstopnlem1  23934  xkohmeo  23940  prdstmdd  24249  ucnimalem  24404  fmucndlem  24415  fsum2cn  24998  ovoliunlem1  25629  lgsquadlem1  27509  lgsquadlem2  27510  2sqreuop  27591  2sqreuopnn  27592  2sqreuoplt  27593  2sqreuopltb  27594  2sqreuopnnlt  27595  2sqreuopnnltb  27596  clwlkclwwlkfolem  30298  wlkl0  30658  gsumhashmul  33327  gsumwrd2dccatlem  33337  gsumwrd2dccat  33338  conjga  33430  elrgspnlem2  33503  elrgspnsubrunlem2  33508  mplvrpmga  33879  eulerpartlemgs2  34714  hgt750lemb  34987  cvmliftlem15  35688  satfv1  35753  satfdmlem  35758  fmlasuc  35776  msubty  35917  msubco  35921  msubvrs  35950  nmulprop  36580  filnetlem4  36780  finixpnum  38143  poimirlem4  38162  poimirlem15  38173  poimirlem20  38178  poimirlem26  38184  poimirlem28  38186  heicant  38193  dicelvalN  41841  aks6d1c2p1  42774  aks6d1c3  42779  aks6d1c4  42780  aks6d1c6lem2  42827  aks6d1c6lem4  42829  aks6d1c7lem1  42836  fmpocos  42893  rmxypairf1o  43529  unxpwdom3  43713  fgraphxp  43822  elcnvlem  44218  dvnprodlem2  46552  etransclem46  46885  ovnsubaddlem1  47175  gpgvtxedg0  48716  gpgvtxedg1  48717  gpgcubic  48732  gpg5nbgr3star  48734  pgnbgreunbgrlem3  48771  pgnbgreunbgrlem6  48777  dmmpossx2  49001  2arymaptf  49316  rrx2plordisom  49387  eloprab1st2nd  49530  funcf2lem  49743  oppf1  49801  tposcurf1  49961  reldmprcof1  50043  opf11  50065  setc1ocofval  50156