Theorem op1std 7873

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  Vcvv 3437  ⟨cop 4571  ‘cfv 6458  1^st c1st 7861

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-iota 6410  df-fun 6460  df-fv 6466  df-1st 7863

This theorem is referenced by:  1st2val  7891  xp1st  7895  sbcopeq1a  7922  csbopeq1a  7923  eloprabi  7935  mpomptsx  7936  dmmpossx  7938  fmpox  7939  ovmptss  7965  fmpoco  7967  df1st2  7970  fsplit  7989  frxp  7998  xporderlem  7999  fnwelem  8003  fimaproj  8007  xpf1o  8964  mapunen  8971  xpwdomg  9388  hsmexlem2  10229  fsumcom2  15531  fprodcom2  15739  qredeu  16408  isfuncd  17625  cofucl  17648  funcres2b  17657  funcpropd  17661  xpcco1st  17946  xpccatid  17950  1stf1  17954  2ndf1  17957  1stfcl  17959  prf1  17962  prfcl  17965  prf1st  17966  prf2nd  17967  evlf1  17983  evlfcl  17985  curf1fval  17987  curf11  17989  curf1cl  17991  curfcl  17995  hof1fval  18016  txbas  22763  cnmpt1st  22864  txhmeo  22999  ptuncnv  23003  ptunhmeo  23004  xpstopnlem1  23005  xkohmeo  23011  prdstmdd  23320  ucnimalem  23477  fmucndlem  23488  fsum2cn  24079  ovoliunlem1  24711  lgsquadlem1  26573  lgsquadlem2  26574  2sqreuop  26655  2sqreuopnn  26656  2sqreuoplt  26657  2sqreuopltb  26658  2sqreuopnnlt  26659  2sqreuopnnltb  26660  clwlkclwwlkfolem  28416  wlkl0  28776  gsumhashmul  31361  eulerpartlemgs2  32392  hgt750lemb  32681  cvmliftlem15  33305  satfv1  33370  satfdmlem  33375  fmlasuc  33393  msubty  33534  msubco  33538  msubvrs  33567  ot21std  33725  ot22ndd  33726  xpord2lem  33834  naddcllem  33876  filnetlem4  34615  finixpnum  35806  poimirlem4  35825  poimirlem15  35836  poimirlem20  35841  poimirlem26  35847  poimirlem28  35849  heicant  35856  dicelvalN  39234  rmxypairf1o  40771  unxpwdom3  40958  fgraphxp  41074  elcnvlem  41247  dvnprodlem2  43537  etransclem46  43870  ovnsubaddlem1  44158  dmmpossx2  45730  2arymaptf  46056  rrx2plordisom  46127  funcf2lem  46357