Theorem op1std 7681

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ⟨cop 4531  ‘cfv 6324  1^st c1st 7669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fv 6332  df-1st 7671

This theorem is referenced by:  1st2val  7699  xp1st  7703  sbcopeq1a  7730  csbopeq1a  7731  eloprabi  7743  mpomptsx  7744  dmmpossx  7746  fmpox  7747  ovmptss  7771  fmpoco  7773  df1st2  7776  fsplit  7795  fsplitOLD  7796  frxp  7803  xporderlem  7804  fnwelem  7808  fimaproj  7812  xpf1o  8663  mapunen  8670  xpwdomg  9033  hsmexlem2  9838  fsumcom2  15121  fprodcom2  15330  qredeu  15992  isfuncd  17127  cofucl  17150  funcres2b  17159  funcpropd  17162  xpcco1st  17426  xpccatid  17430  1stf1  17434  2ndf1  17437  1stfcl  17439  prf1  17442  prfcl  17445  prf1st  17446  prf2nd  17447  evlf1  17462  evlfcl  17464  curf1fval  17466  curf11  17468  curf1cl  17470  curfcl  17474  hof1fval  17495  txbas  22172  cnmpt1st  22273  txhmeo  22408  ptuncnv  22412  ptunhmeo  22413  xpstopnlem1  22414  xkohmeo  22420  prdstmdd  22729  ucnimalem  22886  fmucndlem  22897  fsum2cn  23476  ovoliunlem1  24106  lgsquadlem1  25964  lgsquadlem2  25965  2sqreuop  26046  2sqreuopnn  26047  2sqreuoplt  26048  2sqreuopltb  26049  2sqreuopnnlt  26050  2sqreuopnnltb  26051  clwlkclwwlkfolem  27792  wlkl0  28152  gsumhashmul  30741  eulerpartlemgs2  31748  hgt750lemb  32037  cvmliftlem15  32658  satfv1  32723  satfdmlem  32728  fmlasuc  32746  msubty  32887  msubco  32891  msubvrs  32920  filnetlem4  33842  finixpnum  35042  poimirlem4  35061  poimirlem15  35072  poimirlem20  35077  poimirlem26  35083  poimirlem28  35085  heicant  35092  dicelvalN  38474  rmxypairf1o  39852  unxpwdom3  40039  fgraphxp  40155  elcnvlem  40301  dvnprodlem2  42589  etransclem46  42922  ovnsubaddlem1  43209  dmmpossx2  44738  2arymaptf  45066  rrx2plordisom  45137