Theorem op1std 7953

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ⟨cop 4588  ‘cfv 6500  1^st c1st 7941

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943

This theorem is referenced by:  1st2val  7971  xp1st  7975  sbcopeq1a  8003  csbopeq1a  8004  eloprabi  8017  mpomptsx  8018  dmmpossx  8020  fmpox  8021  ovmptss  8045  fmpoco  8047  df1st2  8050  fsplit  8069  frxp  8078  xporderlem  8079  fnwelem  8083  fimaproj  8087  xpord2lem  8094  naddcllem  8614  xpf1o  9079  mapunen  9086  xpwdomg  9502  hsmexlem2  10349  fsumcom2  15709  fprodcom2  15919  qredeu  16597  isfuncd  17801  cofucl  17824  funcres2b  17833  funcpropd  17838  xpcco1st  18119  xpccatid  18123  1stf1  18127  2ndf1  18130  1stfcl  18132  prf1  18135  prfcl  18138  prf1st  18139  prf2nd  18140  evlf1  18155  evlfcl  18157  curf1fval  18159  curf11  18161  curf1cl  18163  curfcl  18167  hof1fval  18188  txbas  23523  cnmpt1st  23624  txhmeo  23759  ptuncnv  23763  ptunhmeo  23764  xpstopnlem1  23765  xkohmeo  23771  prdstmdd  24080  ucnimalem  24235  fmucndlem  24246  fsum2cn  24830  ovoliunlem1  25471  lgsquadlem1  27359  lgsquadlem2  27360  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  clwlkclwwlkfolem  30094  wlkl0  30454  gsumhashmul  33161  gsumwrd2dccatlem  33171  gsumwrd2dccat  33172  conjga  33264  elrgspnlem2  33337  elrgspnsubrunlem2  33342  mplvrpmga  33722  eulerpartlemgs2  34558  hgt750lemb  34834  cvmliftlem15  35514  satfv1  35579  satfdmlem  35584  fmlasuc  35602  msubty  35743  msubco  35747  msubvrs  35776  filnetlem4  36597  finixpnum  37856  poimirlem4  37875  poimirlem15  37886  poimirlem20  37891  poimirlem26  37897  poimirlem28  37899  heicant  37906  dicelvalN  41554  aks6d1c2p1  42488  aks6d1c3  42493  aks6d1c4  42494  aks6d1c6lem2  42541  aks6d1c6lem4  42543  aks6d1c7lem1  42550  fmpocos  42606  rmxypairf1o  43268  unxpwdom3  43452  fgraphxp  43561  elcnvlem  43957  dvnprodlem2  46305  etransclem46  46638  ovnsubaddlem1  46928  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgcubic  48439  gpg5nbgr3star  48441  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  dmmpossx2  48697  2arymaptf  49012  rrx2plordisom  49083  eloprab1st2nd  49227  funcf2lem  49440  oppf1  49498  tposcurf1  49658  reldmprcof1  49740  opf11  49762  setc1ocofval  49853