Theorem op1std 7943

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ⟨cop 4586  ‘cfv 6492  1^st c1st 7931

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7933

This theorem is referenced by:  1st2val  7961  xp1st  7965  sbcopeq1a  7993  csbopeq1a  7994  eloprabi  8007  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8035  fmpoco  8037  df1st2  8040  fsplit  8059  frxp  8068  xporderlem  8069  fnwelem  8073  fimaproj  8077  xpord2lem  8084  naddcllem  8604  xpf1o  9067  mapunen  9074  xpwdomg  9490  hsmexlem2  10337  fsumcom2  15697  fprodcom2  15907  qredeu  16585  isfuncd  17789  cofucl  17812  funcres2b  17821  funcpropd  17826  xpcco1st  18107  xpccatid  18111  1stf1  18115  2ndf1  18118  1stfcl  18120  prf1  18123  prfcl  18126  prf1st  18127  prf2nd  18128  evlf1  18143  evlfcl  18145  curf1fval  18147  curf11  18149  curf1cl  18151  curfcl  18155  hof1fval  18176  txbas  23511  cnmpt1st  23612  txhmeo  23747  ptuncnv  23751  ptunhmeo  23752  xpstopnlem1  23753  xkohmeo  23759  prdstmdd  24068  ucnimalem  24223  fmucndlem  24234  fsum2cn  24818  ovoliunlem1  25459  lgsquadlem1  27347  lgsquadlem2  27348  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  clwlkclwwlkfolem  30082  wlkl0  30442  gsumhashmul  33150  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  conjga  33252  elrgspnlem2  33325  elrgspnsubrunlem2  33330  mplvrpmga  33710  eulerpartlemgs2  34537  hgt750lemb  34813  cvmliftlem15  35492  satfv1  35557  satfdmlem  35562  fmlasuc  35580  msubty  35721  msubco  35725  msubvrs  35754  filnetlem4  36575  finixpnum  37806  poimirlem4  37825  poimirlem15  37836  poimirlem20  37841  poimirlem26  37847  poimirlem28  37849  heicant  37856  dicelvalN  41438  aks6d1c2p1  42372  aks6d1c3  42377  aks6d1c4  42378  aks6d1c6lem2  42425  aks6d1c6lem4  42427  aks6d1c7lem1  42434  fmpocos  42490  rmxypairf1o  43153  unxpwdom3  43337  fgraphxp  43446  elcnvlem  43842  dvnprodlem2  46191  etransclem46  46524  ovnsubaddlem1  46814  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgcubic  48325  gpg5nbgr3star  48327  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  dmmpossx2  48583  2arymaptf  48898  rrx2plordisom  48969  eloprab1st2nd  49113  funcf2lem  49326  oppf1  49384  tposcurf1  49544  reldmprcof1  49626  opf11  49648  setc1ocofval  49739