Theorem op1std 8002

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3457  ⟨cop 4597  ‘cfv 6540  1^st c1st 7990

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fv 6548  df-1st 7992

This theorem is used by:  1st2val  8020  xp1st  8024  sbcopeq1a  8052  csbopeq1a  8053  eloprabi  8066  mpomptsx  8067  dmmpossx  8069  fmpox  8070  ovmptss  8094  fmpoco  8096  df1st2  8099  fsplit  8118  frxp  8128  xporderlem  8129  fnwelem  8133  fimaproj  8137  xpord2lem  8144  naddcllem  8668  xpf1o  9134  mapunen  9141  xpwdomg  9554  hsmexlem2  10426  fsumcom2  15848  fprodcom2  16061  qredeu  16738  isfuncd  17944  cofucl  17967  funcres2b  17976  funcpropd  17981  xpcco1st  18262  xpccatid  18266  1stf1  18270  2ndf1  18273  1stfcl  18275  prf1  18278  prfcl  18281  prf1st  18282  prf2nd  18283  evlf1  18298  evlfcl  18300  curf1fval  18302  curf11  18304  curf1cl  18306  curfcl  18310  hof1fval  18331  txbas  23775  cnmpt1st  23876  txhmeo  24011  ptuncnv  24015  ptunhmeo  24016  xpstopnlem1  24017  xkohmeo  24023  prdstmdd  24332  ucnimalem  24487  fmucndlem  24498  fsum2cn  25081  ovoliunlem1  25712  lgsquadlem1  27595  lgsquadlem2  27596  2sqreuop  27677  2sqreuopnn  27678  2sqreuoplt  27679  2sqreuopltb  27680  2sqreuopnnlt  27681  2sqreuopnnltb  27682  clwlkclwwlkfolem  30425  wlkl0  30789  gsumhashmul  33451  gsumwrd2dccatlem  33461  gsumwrd2dccat  33462  conjga  33554  elrgspnlem2  33627  elrgspnsubrunlem2  33632  mplvrpmga  33999  eulerpartlemgs2  34835  hgt750lemb  35108  cvmliftlem15  35827  satfv1  35892  satfdmlem  35897  fmlasuc  35915  msubty  36056  msubco  36060  msubvrs  36089  nmulprop  36719  filnetlem4  36949  finixpnum  38313  poimirlem4  38332  poimirlem15  38343  poimirlem20  38348  poimirlem26  38354  poimirlem28  38356  heicant  38363  dicelvalN  42010  aks6d1c2p1  42943  aks6d1c3  42948  aks6d1c4  42949  aks6d1c6lem2  42996  aks6d1c6lem4  42998  aks6d1c7lem1  43005  fmpocos  43062  rmxypairf1o  43696  unxpwdom3  43880  fgraphxp  43989  elcnvlem  44385  dvnprodlem2  46719  etransclem46  47052  ovnsubaddlem1  47342  gpgvtxedg0  48886  gpgvtxedg1  48887  gpgcubic  48902  gpg5nbgr3star  48904  pgnbgreunbgrlem3  48941  pgnbgreunbgrlem6  48947  dmmpossx2  49174  2arymaptf  49489  rrx2plordisom  49560  eloprab1st2nd  49703  funcf2lem  49916  oppf1  49974  tposcurf1  50134  reldmprcof1  50216  opf11  50238  setc1ocofval  50329