Theorem op1std 7952

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ⟨cop 4573  ‘cfv 6498  1^st c1st 7940

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fv 6506  df-1st 7942

This theorem is referenced by:  1st2val  7970  xp1st  7974  sbcopeq1a  8002  csbopeq1a  8003  eloprabi  8016  mpomptsx  8017  dmmpossx  8019  fmpox  8020  ovmptss  8043  fmpoco  8045  df1st2  8048  fsplit  8067  frxp  8076  xporderlem  8077  fnwelem  8081  fimaproj  8085  xpord2lem  8092  naddcllem  8612  xpf1o  9077  mapunen  9084  xpwdomg  9500  hsmexlem2  10349  fsumcom2  15736  fprodcom2  15949  qredeu  16627  isfuncd  17832  cofucl  17855  funcres2b  17864  funcpropd  17869  xpcco1st  18150  xpccatid  18154  1stf1  18158  2ndf1  18161  1stfcl  18163  prf1  18166  prfcl  18169  prf1st  18170  prf2nd  18171  evlf1  18186  evlfcl  18188  curf1fval  18190  curf11  18192  curf1cl  18194  curfcl  18198  hof1fval  18219  txbas  23532  cnmpt1st  23633  txhmeo  23768  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  xkohmeo  23780  prdstmdd  24089  ucnimalem  24244  fmucndlem  24255  fsum2cn  24838  ovoliunlem1  25469  lgsquadlem1  27343  lgsquadlem2  27344  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  clwlkclwwlkfolem  30077  wlkl0  30437  gsumhashmul  33128  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  conjga  33231  elrgspnlem2  33304  elrgspnsubrunlem2  33309  mplvrpmga  33689  eulerpartlemgs2  34524  hgt750lemb  34800  cvmliftlem15  35480  satfv1  35545  satfdmlem  35550  fmlasuc  35568  msubty  35709  msubco  35713  msubvrs  35742  filnetlem4  36563  finixpnum  37926  poimirlem4  37945  poimirlem15  37956  poimirlem20  37961  poimirlem26  37967  poimirlem28  37969  heicant  37976  dicelvalN  41624  aks6d1c2p1  42557  aks6d1c3  42562  aks6d1c4  42563  aks6d1c6lem2  42610  aks6d1c6lem4  42612  aks6d1c7lem1  42619  fmpocos  42675  rmxypairf1o  43339  unxpwdom3  43523  fgraphxp  43632  elcnvlem  44028  dvnprodlem2  46375  etransclem46  46708  ovnsubaddlem1  46998  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgcubic  48555  gpg5nbgr3star  48557  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  dmmpossx2  48813  2arymaptf  49128  rrx2plordisom  49199  eloprab1st2nd  49343  funcf2lem  49556  oppf1  49614  tposcurf1  49774  reldmprcof1  49856  opf11  49878  setc1ocofval  49969