Theorem op1std 7691

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 6663	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1st 7689	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
5	1, 4	syl6eq 2870	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)

Syntax hints:   → wi 4   = wceq 1530   ∈ wcel 2107  Vcvv 3493  ⟨cop 4565  ‘cfv 6348  1^st c1st 7679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fv 6356  df-1st 7681

This theorem is referenced by:  1st2val  7709  xp1st  7713  sbcopeq1a  7740  csbopeq1a  7741  eloprabi  7753  mpomptsx  7754  dmmpossx  7756  fmpox  7757  ovmptss  7780  fmpoco  7782  df1st2  7785  fsplit  7804  fsplitOLD  7805  frxp  7812  xporderlem  7813  fnwelem  7817  fimaproj  7821  xpf1o  8671  mapunen  8678  xpwdomg  9041  hsmexlem2  9841  fsumcom2  15121  fprodcom2  15330  qredeu  15994  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  22167  cnmpt1st  22268  txhmeo  22403  ptuncnv  22407  ptunhmeo  22408  xpstopnlem1  22409  xkohmeo  22415  prdstmdd  22724  ucnimalem  22881  fmucndlem  22892  fsum2cn  23471  ovoliunlem1  24095  lgsquadlem1  25948  lgsquadlem2  25949  2sqreuop  26030  2sqreuopnn  26031  2sqreuoplt  26032  2sqreuopltb  26033  2sqreuopnnlt  26034  2sqreuopnnltb  26035  clwlkclwwlkfolem  27777  wlkl0  28138  eulerpartlemgs2  31631  hgt750lemb  31920  cvmliftlem15  32538  satfv1  32603  satfdmlem  32608  fmlasuc  32626  msubty  32767  msubco  32771  msubvrs  32800  filnetlem4  33722  finixpnum  34869  poimirlem4  34888  poimirlem15  34899  poimirlem20  34904  poimirlem26  34910  poimirlem28  34912  heicant  34919  dicelvalN  38306  rmxypairf1o  39498  unxpwdom3  39685  fgraphxp  39801  elcnvlem  39951  dvnprodlem2  42221  etransclem46  42555  ovnsubaddlem1  42842  dmmpossx2  44375  rrx2plordisom  44700