Theorem op1std 7996

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fv 6541  df-1st 7986

This theorem is used by:  1st2val  8014  xp1st  8018  sbcopeq1a  8046  csbopeq1a  8047  eloprabi  8060  mpomptsx  8061  dmmpossx  8063  fmpox  8064  ovmptss  8090  fmpoco  8092  df1st2  8095  fsplit  8114  frxp  8124  xporderlem  8125  fnwelem  8129  fimaproj  8133  xpord2lem  8140  naddcllem  8664  xpf1o  9137  mapunen  9144  xpwdomg  9557  hsmexlem2  10429  fsumcom2  15860  fprodcom2  16071  qredeu  16748  isfuncd  17954  cofucl  17977  funcres2b  17986  funcpropd  17991  xpcco1st  18272  xpccatid  18276  1stf1  18280  2ndf1  18283  1stfcl  18285  prf1  18288  prfcl  18291  prf1st  18292  prf2nd  18293  evlf1  18308  evlfcl  18310  curf1fval  18312  curf11  18314  curf1cl  18316  curfcl  18320  hof1fval  18341  txbas  23793  cnmpt1st  23894  txhmeo  24029  ptuncnv  24033  ptunhmeo  24034  xpstopnlem1  24035  xkohmeo  24041  prdstmdd  24350  ucnimalem  24505  fmucndlem  24516  fsum2cn  25099  ovoliunlem1  25730  lgsquadlem1  27616  lgsquadlem2  27617  2sqreuop  27698  2sqreuopnn  27699  2sqreuoplt  27700  2sqreuopltb  27701  2sqreuopnnlt  27702  2sqreuopnnltb  27703  clwlkclwwlkfolem  30477  wlkl0  30847  gsumhashmul  33507  gsumwrd2dccatlem  33517  gsumwrd2dccat  33518  conjga  33610  elrgspnlem2  33683  elrgspnsubrunlem2  33688  mplvrpmga  34055  eulerpartlemgs2  34891  hgt750lemb  35164  cvmliftlem15  35877  satfv1  35942  satfdmlem  35947  fmlasuc  35965  msubty  36106  msubco  36110  msubvrs  36139  nmulprop  36770  filnetlem4  37000  finixpnum  38359  poimirlem4  38373  poimirlem15  38384  poimirlem20  38389  poimirlem26  38395  poimirlem28  38397  heicant  38404  dicelvalN  42051  aks6d1c2p1  42984  aks6d1c3  42989  aks6d1c4  42990  aks6d1c6lem2  43037  aks6d1c6lem4  43039  aks6d1c7lem1  43046  fmpocos  43103  rmxypairf1o  43752  unxpwdom3  43936  fgraphxp  44045  elcnvlem  44441  dvnprodlem2  46775  etransclem46  47108  ovnsubaddlem1  47398  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgcubic  48995  gpg5nbgr3star  48997  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  dmmpossx2  49267  2arymaptf  49582  rrx2plordisom  49653  eloprab1st2nd  49796  funcf2lem  50007  oppf1  50065  tposcurf1  50225  reldmprcof1  50307  opf11  50329  setc1ocofval  50420