Theorem op1std 7934

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ⟨cop 4583  ‘cfv 6482  1^st c1st 7922

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fv 6490  df-1st 7924

This theorem is referenced by:  1st2val  7952  xp1st  7956  sbcopeq1a  7984  csbopeq1a  7985  eloprabi  7998  mpomptsx  7999  dmmpossx  8001  fmpox  8002  ovmptss  8026  fmpoco  8028  df1st2  8031  fsplit  8050  frxp  8059  xporderlem  8060  fnwelem  8064  fimaproj  8068  xpord2lem  8075  naddcllem  8594  xpf1o  9056  mapunen  9063  xpwdomg  9477  hsmexlem2  10321  fsumcom2  15681  fprodcom2  15891  qredeu  16569  isfuncd  17772  cofucl  17795  funcres2b  17804  funcpropd  17809  xpcco1st  18090  xpccatid  18094  1stf1  18098  2ndf1  18101  1stfcl  18103  prf1  18106  prfcl  18109  prf1st  18110  prf2nd  18111  evlf1  18126  evlfcl  18128  curf1fval  18130  curf11  18132  curf1cl  18134  curfcl  18138  hof1fval  18159  txbas  23452  cnmpt1st  23553  txhmeo  23688  ptuncnv  23692  ptunhmeo  23693  xpstopnlem1  23694  xkohmeo  23700  prdstmdd  24009  ucnimalem  24165  fmucndlem  24176  fsum2cn  24760  ovoliunlem1  25401  lgsquadlem1  27289  lgsquadlem2  27290  2sqreuop  27371  2sqreuopnn  27372  2sqreuoplt  27373  2sqreuopltb  27374  2sqreuopnnlt  27375  2sqreuopnnltb  27376  clwlkclwwlkfolem  29951  wlkl0  30311  gsumhashmul  33014  gsumwrd2dccatlem  33019  gsumwrd2dccat  33020  conjga  33112  elrgspnlem2  33183  elrgspnsubrunlem2  33188  mplvrpmga  33546  eulerpartlemgs2  34348  hgt750lemb  34624  cvmliftlem15  35271  satfv1  35336  satfdmlem  35341  fmlasuc  35359  msubty  35500  msubco  35504  msubvrs  35533  filnetlem4  36355  finixpnum  37585  poimirlem4  37604  poimirlem15  37615  poimirlem20  37620  poimirlem26  37626  poimirlem28  37628  heicant  37635  dicelvalN  41157  aks6d1c2p1  42091  aks6d1c3  42096  aks6d1c4  42097  aks6d1c6lem2  42144  aks6d1c6lem4  42146  aks6d1c7lem1  42153  fmpocos  42207  rmxypairf1o  42884  unxpwdom3  43068  fgraphxp  43177  elcnvlem  43574  dvnprodlem2  45928  etransclem46  46261  ovnsubaddlem1  46551  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgcubic  48063  gpg5nbgr3star  48065  pgnbgreunbgrlem3  48102  pgnbgreunbgrlem6  48108  dmmpossx2  48321  2arymaptf  48637  rrx2plordisom  48708  eloprab1st2nd  48852  funcf2lem  49066  oppf1  49124  tposcurf1  49284  reldmprcof1  49366  opf11  49388  setc1ocofval  49479