Theorem op1std 7945

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3441  ⟨cop 4587  ‘cfv 6493  1^st c1st 7933

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-1st 7935

This theorem is referenced by:  1st2val  7963  xp1st  7967  sbcopeq1a  7995  csbopeq1a  7996  eloprabi  8009  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8037  fmpoco  8039  df1st2  8042  fsplit  8061  frxp  8070  xporderlem  8071  fnwelem  8075  fimaproj  8079  xpord2lem  8086  naddcllem  8606  xpf1o  9071  mapunen  9078  xpwdomg  9494  hsmexlem2  10341  fsumcom2  15701  fprodcom2  15911  qredeu  16589  isfuncd  17793  cofucl  17816  funcres2b  17825  funcpropd  17830  xpcco1st  18111  xpccatid  18115  1stf1  18119  2ndf1  18122  1stfcl  18124  prf1  18127  prfcl  18130  prf1st  18131  prf2nd  18132  evlf1  18147  evlfcl  18149  curf1fval  18151  curf11  18153  curf1cl  18155  curfcl  18159  hof1fval  18180  txbas  23515  cnmpt1st  23616  txhmeo  23751  ptuncnv  23755  ptunhmeo  23756  xpstopnlem1  23757  xkohmeo  23763  prdstmdd  24072  ucnimalem  24227  fmucndlem  24238  fsum2cn  24822  ovoliunlem1  25463  lgsquadlem1  27351  lgsquadlem2  27352  2sqreuop  27433  2sqreuopnn  27434  2sqreuoplt  27435  2sqreuopltb  27436  2sqreuopnnlt  27437  2sqreuopnnltb  27438  clwlkclwwlkfolem  30065  wlkl0  30425  gsumhashmul  33131  gsumwrd2dccatlem  33140  gsumwrd2dccat  33141  conjga  33233  elrgspnlem2  33306  elrgspnsubrunlem2  33311  mplvrpmga  33691  eulerpartlemgs2  34518  hgt750lemb  34794  cvmliftlem15  35473  satfv1  35538  satfdmlem  35543  fmlasuc  35561  msubty  35702  msubco  35706  msubvrs  35735  filnetlem4  36556  finixpnum  37777  poimirlem4  37796  poimirlem15  37807  poimirlem20  37812  poimirlem26  37818  poimirlem28  37820  heicant  37827  dicelvalN  41475  aks6d1c2p1  42409  aks6d1c3  42414  aks6d1c4  42415  aks6d1c6lem2  42462  aks6d1c6lem4  42464  aks6d1c7lem1  42471  fmpocos  42527  rmxypairf1o  43189  unxpwdom3  43373  fgraphxp  43482  elcnvlem  43878  dvnprodlem2  46227  etransclem46  46560  ovnsubaddlem1  46850  gpgvtxedg0  48345  gpgvtxedg1  48346  gpgcubic  48361  gpg5nbgr3star  48363  pgnbgreunbgrlem3  48400  pgnbgreunbgrlem6  48406  dmmpossx2  48619  2arymaptf  48934  rrx2plordisom  49005  eloprab1st2nd  49149  funcf2lem  49362  oppf1  49420  tposcurf1  49580  reldmprcof1  49662  opf11  49684  setc1ocofval  49775