Theorem op1std 7957

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ⟨cop 4591  ‘cfv 6499  1^st c1st 7945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fv 6507  df-1st 7947

This theorem is referenced by:  1st2val  7975  xp1st  7979  sbcopeq1a  8007  csbopeq1a  8008  eloprabi  8021  mpomptsx  8022  dmmpossx  8024  fmpox  8025  ovmptss  8049  fmpoco  8051  df1st2  8054  fsplit  8073  frxp  8082  xporderlem  8083  fnwelem  8087  fimaproj  8091  xpord2lem  8098  naddcllem  8617  xpf1o  9080  mapunen  9087  xpwdomg  9514  hsmexlem2  10356  fsumcom2  15716  fprodcom2  15926  qredeu  16604  isfuncd  17803  cofucl  17826  funcres2b  17835  funcpropd  17840  xpcco1st  18121  xpccatid  18125  1stf1  18129  2ndf1  18132  1stfcl  18134  prf1  18137  prfcl  18140  prf1st  18141  prf2nd  18142  evlf1  18157  evlfcl  18159  curf1fval  18161  curf11  18163  curf1cl  18165  curfcl  18169  hof1fval  18190  txbas  23430  cnmpt1st  23531  txhmeo  23666  ptuncnv  23670  ptunhmeo  23671  xpstopnlem1  23672  xkohmeo  23678  prdstmdd  23987  ucnimalem  24143  fmucndlem  24154  fsum2cn  24738  ovoliunlem1  25379  lgsquadlem1  27267  lgsquadlem2  27268  2sqreuop  27349  2sqreuopnn  27350  2sqreuoplt  27351  2sqreuopltb  27352  2sqreuopnnlt  27353  2sqreuopnnltb  27354  clwlkclwwlkfolem  29909  wlkl0  30269  gsumhashmul  32974  gsumwrd2dccatlem  32979  gsumwrd2dccat  32980  conjga  33100  elrgspnlem2  33167  elrgspnsubrunlem2  33172  eulerpartlemgs2  34344  hgt750lemb  34620  cvmliftlem15  35258  satfv1  35323  satfdmlem  35328  fmlasuc  35346  msubty  35487  msubco  35491  msubvrs  35520  filnetlem4  36342  finixpnum  37572  poimirlem4  37591  poimirlem15  37602  poimirlem20  37607  poimirlem26  37613  poimirlem28  37615  heicant  37622  dicelvalN  41145  aks6d1c2p1  42079  aks6d1c3  42084  aks6d1c4  42085  aks6d1c6lem2  42132  aks6d1c6lem4  42134  aks6d1c7lem1  42141  fmpocos  42195  rmxypairf1o  42873  unxpwdom3  43057  fgraphxp  43166  elcnvlem  43563  dvnprodlem2  45918  etransclem46  46251  ovnsubaddlem1  46541  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgcubic  48043  gpg5nbgr3star  48045  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  dmmpossx2  48298  2arymaptf  48614  rrx2plordisom  48685  eloprab1st2nd  48829  funcf2lem  49043  oppf1  49101  tposcurf1  49261  reldmprcof1  49343  opf11  49365  setc1ocofval  49456