Theorem op1std 7989

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  Vcvv 3473  ⟨cop 4634  ‘cfv 6543  1^st c1st 7977

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fv 6551  df-1st 7979

This theorem is referenced by:  1st2val  8007  xp1st  8011  sbcopeq1a  8039  csbopeq1a  8040  eloprabi  8053  mpomptsx  8054  dmmpossx  8056  fmpox  8057  ovmptss  8084  fmpoco  8086  df1st2  8089  fsplit  8108  frxp  8117  xporderlem  8118  fnwelem  8122  fimaproj  8126  xpord2lem  8133  naddcllem  8681  xpf1o  9145  mapunen  9152  xpwdomg  9586  hsmexlem2  10428  fsumcom2  15727  fprodcom2  15935  qredeu  16602  isfuncd  17822  cofucl  17845  funcres2b  17854  funcpropd  17860  xpcco1st  18146  xpccatid  18150  1stf1  18154  2ndf1  18157  1stfcl  18159  prf1  18162  prfcl  18165  prf1st  18166  prf2nd  18167  evlf1  18183  evlfcl  18185  curf1fval  18187  curf11  18189  curf1cl  18191  curfcl  18195  hof1fval  18216  txbas  23391  cnmpt1st  23492  txhmeo  23627  ptuncnv  23631  ptunhmeo  23632  xpstopnlem1  23633  xkohmeo  23639  prdstmdd  23948  ucnimalem  24105  fmucndlem  24116  fsum2cn  24709  ovoliunlem1  25351  lgsquadlem1  27226  lgsquadlem2  27227  2sqreuop  27308  2sqreuopnn  27309  2sqreuoplt  27310  2sqreuopltb  27311  2sqreuopnnlt  27312  2sqreuopnnltb  27313  clwlkclwwlkfolem  29693  wlkl0  30053  gsumhashmul  32644  eulerpartlemgs2  33843  hgt750lemb  34132  cvmliftlem15  34753  satfv1  34818  satfdmlem  34823  fmlasuc  34841  msubty  34982  msubco  34986  msubvrs  35015  filnetlem4  35730  finixpnum  36937  poimirlem4  36956  poimirlem15  36967  poimirlem20  36972  poimirlem26  36978  poimirlem28  36980  heicant  36987  dicelvalN  40513  aks6d1c2p1  41423  fmpocos  41523  rmxypairf1o  42113  unxpwdom3  42300  fgraphxp  42416  elcnvlem  42815  dvnprodlem2  45122  etransclem46  45455  ovnsubaddlem1  45745  dmmpossx2  47175  2arymaptf  47500  rrx2plordisom  47571  funcf2lem  47800