Theorem op1std 7941

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ⟨cop 4561  ‘cfv 6485  1^st c1st 7929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fv 6493  df-1st 7931

This theorem is referenced by:  1st2val  7959  xp1st  7963  sbcopeq1a  7991  csbopeq1a  7992  eloprabi  8005  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8032  fmpoco  8034  df1st2  8037  fsplit  8056  frxp  8066  xporderlem  8067  fnwelem  8071  fimaproj  8075  xpord2lem  8082  naddcllem  8602  xpf1o  9067  mapunen  9074  xpwdomg  9490  hsmexlem2  10340  fsumcom2  15727  fprodcom2  15940  qredeu  16618  isfuncd  17823  cofucl  17846  funcres2b  17855  funcpropd  17860  xpcco1st  18141  xpccatid  18145  1stf1  18149  2ndf1  18152  1stfcl  18154  prf1  18157  prfcl  18160  prf1st  18161  prf2nd  18162  evlf1  18177  evlfcl  18179  curf1fval  18181  curf11  18183  curf1cl  18185  curfcl  18189  hof1fval  18210  txbas  23550  cnmpt1st  23651  txhmeo  23786  ptuncnv  23790  ptunhmeo  23791  xpstopnlem1  23792  xkohmeo  23798  prdstmdd  24107  ucnimalem  24262  fmucndlem  24273  fsum2cn  24856  ovoliunlem1  25487  lgsquadlem1  27361  lgsquadlem2  27362  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  clwlkclwwlkfolem  30095  wlkl0  30455  gsumhashmul  33148  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  conjga  33251  elrgspnlem2  33324  elrgspnsubrunlem2  33329  mplvrpmga  33729  eulerpartlemgs2  34564  hgt750lemb  34840  cvmliftlem15  35526  satfv1  35591  satfdmlem  35596  fmlasuc  35614  msubty  35755  msubco  35759  msubvrs  35788  filnetlem4  36609  finixpnum  37972  poimirlem4  37991  poimirlem15  38002  poimirlem20  38007  poimirlem26  38013  poimirlem28  38015  heicant  38022  dicelvalN  41670  aks6d1c2p1  42603  aks6d1c3  42608  aks6d1c4  42609  aks6d1c6lem2  42656  aks6d1c6lem4  42658  aks6d1c7lem1  42665  fmpocos  42720  rmxypairf1o  43356  unxpwdom3  43540  fgraphxp  43649  elcnvlem  44045  dvnprodlem2  46390  etransclem46  46723  ovnsubaddlem1  47013  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgcubic  48570  gpg5nbgr3star  48572  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  dmmpossx2  48828  2arymaptf  49143  rrx2plordisom  49214  eloprab1st2nd  49358  funcf2lem  49571  oppf1  49629  tposcurf1  49789  reldmprcof1  49871  opf11  49893  setc1ocofval  49984