Theorem op1std 7941

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438  ⟨cop 4584  ‘cfv 6490  1^st c1st 7929

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7931

This theorem is referenced by:  1st2val  7959  xp1st  7963  sbcopeq1a  7991  csbopeq1a  7992  eloprabi  8005  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8033  fmpoco  8035  df1st2  8038  fsplit  8057  frxp  8066  xporderlem  8067  fnwelem  8071  fimaproj  8075  xpord2lem  8082  naddcllem  8602  xpf1o  9065  mapunen  9072  xpwdomg  9488  hsmexlem2  10335  fsumcom2  15695  fprodcom2  15905  qredeu  16583  isfuncd  17787  cofucl  17810  funcres2b  17819  funcpropd  17824  xpcco1st  18105  xpccatid  18109  1stf1  18113  2ndf1  18116  1stfcl  18118  prf1  18121  prfcl  18124  prf1st  18125  prf2nd  18126  evlf1  18141  evlfcl  18143  curf1fval  18145  curf11  18147  curf1cl  18149  curfcl  18153  hof1fval  18174  txbas  23509  cnmpt1st  23610  txhmeo  23745  ptuncnv  23749  ptunhmeo  23750  xpstopnlem1  23751  xkohmeo  23757  prdstmdd  24066  ucnimalem  24221  fmucndlem  24232  fsum2cn  24816  ovoliunlem1  25457  lgsquadlem1  27345  lgsquadlem2  27346  2sqreuop  27427  2sqreuopnn  27428  2sqreuoplt  27429  2sqreuopltb  27430  2sqreuopnnlt  27431  2sqreuopnnltb  27432  clwlkclwwlkfolem  30031  wlkl0  30391  gsumhashmul  33099  gsumwrd2dccatlem  33108  gsumwrd2dccat  33109  conjga  33201  elrgspnlem2  33274  elrgspnsubrunlem2  33279  mplvrpmga  33659  eulerpartlemgs2  34486  hgt750lemb  34762  cvmliftlem15  35441  satfv1  35506  satfdmlem  35511  fmlasuc  35529  msubty  35670  msubco  35674  msubvrs  35703  filnetlem4  36524  finixpnum  37745  poimirlem4  37764  poimirlem15  37775  poimirlem20  37780  poimirlem26  37786  poimirlem28  37788  heicant  37795  dicelvalN  41377  aks6d1c2p1  42311  aks6d1c3  42316  aks6d1c4  42317  aks6d1c6lem2  42364  aks6d1c6lem4  42366  aks6d1c7lem1  42373  fmpocos  42432  rmxypairf1o  43095  unxpwdom3  43279  fgraphxp  43388  elcnvlem  43784  dvnprodlem2  46133  etransclem46  46466  ovnsubaddlem1  46756  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgcubic  48267  gpg5nbgr3star  48269  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  dmmpossx2  48525  2arymaptf  48840  rrx2plordisom  48911  eloprab1st2nd  49055  funcf2lem  49268  oppf1  49326  tposcurf1  49486  reldmprcof1  49568  opf11  49590  setc1ocofval  49681