Theorem op1std 7981

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ⟨cop 4598  ‘cfv 6514  1^st c1st 7969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971

This theorem is referenced by:  1st2val  7999  xp1st  8003  sbcopeq1a  8031  csbopeq1a  8032  eloprabi  8045  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fmpoco  8077  df1st2  8080  fsplit  8099  frxp  8108  xporderlem  8109  fnwelem  8113  fimaproj  8117  xpord2lem  8124  naddcllem  8643  xpf1o  9109  mapunen  9116  xpwdomg  9545  hsmexlem2  10387  fsumcom2  15747  fprodcom2  15957  qredeu  16635  isfuncd  17834  cofucl  17857  funcres2b  17866  funcpropd  17871  xpcco1st  18152  xpccatid  18156  1stf1  18160  2ndf1  18163  1stfcl  18165  prf1  18168  prfcl  18171  prf1st  18172  prf2nd  18173  evlf1  18188  evlfcl  18190  curf1fval  18192  curf11  18194  curf1cl  18196  curfcl  18200  hof1fval  18221  txbas  23461  cnmpt1st  23562  txhmeo  23697  ptuncnv  23701  ptunhmeo  23702  xpstopnlem1  23703  xkohmeo  23709  prdstmdd  24018  ucnimalem  24174  fmucndlem  24185  fsum2cn  24769  ovoliunlem1  25410  lgsquadlem1  27298  lgsquadlem2  27299  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  clwlkclwwlkfolem  29943  wlkl0  30303  gsumhashmul  33008  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  conjga  33134  elrgspnlem2  33201  elrgspnsubrunlem2  33206  eulerpartlemgs2  34378  hgt750lemb  34654  cvmliftlem15  35292  satfv1  35357  satfdmlem  35362  fmlasuc  35380  msubty  35521  msubco  35525  msubvrs  35554  filnetlem4  36376  finixpnum  37606  poimirlem4  37625  poimirlem15  37636  poimirlem20  37641  poimirlem26  37647  poimirlem28  37649  heicant  37656  dicelvalN  41179  aks6d1c2p1  42113  aks6d1c3  42118  aks6d1c4  42119  aks6d1c6lem2  42166  aks6d1c6lem4  42168  aks6d1c7lem1  42175  fmpocos  42229  rmxypairf1o  42907  unxpwdom3  43091  fgraphxp  43200  elcnvlem  43597  dvnprodlem2  45952  etransclem46  46285  ovnsubaddlem1  46575  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgcubic  48074  gpg5nbgr3star  48076  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  dmmpossx2  48329  2arymaptf  48645  rrx2plordisom  48716  eloprab1st2nd  48860  funcf2lem  49074  oppf1  49132  tposcurf1  49292  reldmprcof1  49374  opf11  49396  setc1ocofval  49487