Theorem op1std 7926

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ⟨cop 4577  ‘cfv 6476  1^st c1st 7914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-iota 6432  df-fun 6478  df-fv 6484  df-1st 7916

This theorem is referenced by:  1st2val  7944  xp1st  7948  sbcopeq1a  7976  csbopeq1a  7977  eloprabi  7990  mpomptsx  7991  dmmpossx  7993  fmpox  7994  ovmptss  8018  fmpoco  8020  df1st2  8023  fsplit  8042  frxp  8051  xporderlem  8052  fnwelem  8056  fimaproj  8060  xpord2lem  8067  naddcllem  8586  xpf1o  9047  mapunen  9054  xpwdomg  9466  hsmexlem2  10313  fsumcom2  15676  fprodcom2  15886  qredeu  16564  isfuncd  17767  cofucl  17790  funcres2b  17799  funcpropd  17804  xpcco1st  18085  xpccatid  18089  1stf1  18093  2ndf1  18096  1stfcl  18098  prf1  18101  prfcl  18104  prf1st  18105  prf2nd  18106  evlf1  18121  evlfcl  18123  curf1fval  18125  curf11  18127  curf1cl  18129  curfcl  18133  hof1fval  18154  txbas  23477  cnmpt1st  23578  txhmeo  23713  ptuncnv  23717  ptunhmeo  23718  xpstopnlem1  23719  xkohmeo  23725  prdstmdd  24034  ucnimalem  24189  fmucndlem  24200  fsum2cn  24784  ovoliunlem1  25425  lgsquadlem1  27313  lgsquadlem2  27314  2sqreuop  27395  2sqreuopnn  27396  2sqreuoplt  27397  2sqreuopltb  27398  2sqreuopnnlt  27399  2sqreuopnnltb  27400  clwlkclwwlkfolem  29979  wlkl0  30339  gsumhashmul  33033  gsumwrd2dccatlem  33038  gsumwrd2dccat  33039  conjga  33131  elrgspnlem2  33202  elrgspnsubrunlem2  33207  mplvrpmga  33567  eulerpartlemgs2  34385  hgt750lemb  34661  cvmliftlem15  35334  satfv1  35399  satfdmlem  35404  fmlasuc  35422  msubty  35563  msubco  35567  msubvrs  35596  filnetlem4  36415  finixpnum  37645  poimirlem4  37664  poimirlem15  37675  poimirlem20  37680  poimirlem26  37686  poimirlem28  37688  heicant  37695  dicelvalN  41217  aks6d1c2p1  42151  aks6d1c3  42156  aks6d1c4  42157  aks6d1c6lem2  42204  aks6d1c6lem4  42206  aks6d1c7lem1  42213  fmpocos  42267  rmxypairf1o  42944  unxpwdom3  43128  fgraphxp  43237  elcnvlem  43634  dvnprodlem2  45985  etransclem46  46318  ovnsubaddlem1  46608  gpgvtxedg0  48094  gpgvtxedg1  48095  gpgcubic  48110  gpg5nbgr3star  48112  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155  dmmpossx2  48368  2arymaptf  48684  rrx2plordisom  48755  eloprab1st2nd  48899  funcf2lem  49113  oppf1  49171  tposcurf1  49331  reldmprcof1  49413  opf11  49435  setc1ocofval  49526