Theorem op1std 8009

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ⟨cop 4590  ‘cfv 6537  1^st c1st 7997

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7999

This theorem is used by:  1st2val  8027  xp1st  8031  sbcopeq1a  8058  csbopeq1a  8059  eloprabi  8072  mpomptsx  8073  dmmpossx  8075  fmpox  8076  ovmptss  8102  fmpoco  8104  df1st2  8107  fsplit  8126  frxp  8136  xporderlem  8137  fnwelem  8141  fimaproj  8145  xpord2lem  8152  naddcllem  8678  xpf1o  9151  mapunen  9158  xpwdomg  9572  hsmexlem2  10498  fsumcom2  15933  fprodcom2  16144  qredeu  16826  isfuncd  18033  cofucl  18056  funcres2b  18065  funcpropd  18070  xpcco1st  18351  xpccatid  18355  1stf1  18359  2ndf1  18362  1stfcl  18364  prf1  18367  prfcl  18370  prf1st  18371  prf2nd  18372  evlf1  18387  evlfcl  18389  curf1fval  18391  curf11  18393  curf1cl  18395  curfcl  18399  hof1fval  18420  txbas  23879  cnmpt1st  23980  txhmeo  24115  ptuncnv  24119  ptunhmeo  24120  xpstopnlem1  24121  xkohmeo  24127  prdstmdd  24436  ucnimalem  24591  fmucndlem  24602  fsum2cn  25185  ovoliunlem1  25816  lgsquadlem1  27700  lgsquadlem2  27701  2sqreuop  27782  2sqreuopnn  27783  2sqreuoplt  27784  2sqreuopltb  27785  2sqreuopnnlt  27786  2sqreuopnnltb  27787  clwlkclwwlkfolem  30591  wlkl0  30961  gsumhashmul  33621  gsumwrd2dccatlem  33631  gsumwrd2dccat  33632  conjga  33724  elrgspnlem2  33797  elrgspnsubrunlem2  33802  mplvrpmga  34170  eulerpartlemgs2  35005  hgt750lemb  35278  cvmliftlem15  36042  satfv1  36107  satfdmlem  36112  fmlasuc  36130  msubty  36271  msubco  36275  msubvrs  36304  nmulprop  36919  filnetlem4  37149  finixpnum  38508  poimirlem4  38522  poimirlem15  38533  poimirlem20  38538  poimirlem26  38544  poimirlem28  38546  heicant  38553  dicelvalN  42215  aks6d1c2p1  43148  aks6d1c3  43153  aks6d1c4  43154  aks6d1c6lem2  43201  aks6d1c6lem4  43203  aks6d1c7lem1  43210  fmpocos  43267  rmxypairf1o  43897  unxpwdom3  44081  fgraphxp  44190  elcnvlem  44586  dvnprodlem2  46926  etransclem46  47259  ovnsubaddlem1  47549  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgcubic  49146  gpg5nbgr3star  49148  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  dmmpossx2  49418  2arymaptf  49733  rrx2plordisom  49804  eloprab1st2nd  49947  funcf2lem  50158  oppf1  50216  tposcurf1  50376  reldmprcof1  50458  opf11  50480  setc1ocofval  50571