Theorem op1std 7457

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 6448	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1st 7455	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
5	1, 4	syl6eq 2830	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  Vcvv 3398  ⟨cop 4404  ‘cfv 6137  1^st c1st 7445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-iota 6101  df-fun 6139  df-fv 6145  df-1st 7447

This theorem is referenced by:  1st2val  7475  xp1st  7479  sbcopeq1a  7501  csbopeq1a  7502  eloprabi  7514  mpt2mptsx  7515  dmmpt2ssx  7517  fmpt2x  7518  ovmptss  7541  fmpt2co  7543  df1st2  7546  fsplit  7565  frxp  7570  xporderlem  7571  fnwelem  7575  xpf1o  8412  mapunen  8419  xpwdomg  8781  hsmexlem2  9586  fsumcom2  14919  fprodcom2  15126  qredeu  15787  isfuncd  16921  cofucl  16944  funcres2b  16953  funcpropd  16956  xpcco1st  17221  xpccatid  17225  1stf1  17229  2ndf1  17232  1stfcl  17234  prf1  17237  prfcl  17240  prf1st  17241  prf2nd  17242  evlf1  17257  evlfcl  17259  curf1fval  17261  curf11  17263  curf1cl  17265  curfcl  17269  hof1fval  17290  txbas  21790  cnmpt1st  21891  txhmeo  22026  ptuncnv  22030  ptunhmeo  22031  xpstopnlem1  22032  xkohmeo  22038  prdstmdd  22346  ucnimalem  22503  fmucndlem  22514  fsum2cn  23093  ovoliunlem1  23717  lgsquadlem1  25568  lgsquadlem2  25569  clwlkclwwlkfolem  27408  wlkl0  27812  fimaproj  30506  eulerpartlemgs2  31048  hgt750lemb  31344  cvmliftlem15  31887  msubty  32031  msubco  32035  msubvrs  32064  filnetlem4  32972  finixpnum  34028  poimirlem4  34048  poimirlem15  34059  poimirlem20  34064  poimirlem26  34070  poimirlem28  34072  heicant  34079  dicelvalN  37341  rmxypairf1o  38449  unxpwdom3  38638  fgraphxp  38762  elcnvlem  38878  dvnprodlem2  41104  etransclem46  41438  ovnsubaddlem1  41725  dmmpt2ssx2  43144  rrx2plordisom  43473