Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  op1std Structured version   Visualization version   GIF version

Theorem op1std 7069
 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
StepHypRef Expression
1 fveq2 6103 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (1st𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op1st 7067 . 2 (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
51, 4syl6eq 2660 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (1st𝐶) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ⟨cop 4131  ‘cfv 5804  1st c1st 7057 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fv 5812  df-1st 7059 This theorem is referenced by:  1st2val  7085  xp1st  7089  sbcopeq1a  7111  csbopeq1a  7112  eloprabi  7121  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  ovmptss  7145  fmpt2co  7147  df1st2  7150  fsplit  7169  frxp  7174  xporderlem  7175  fnwelem  7179  xpf1o  8007  mapunen  8014  xpwdomg  8373  hsmexlem2  9132  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  qredeu  15210  isfuncd  16348  cofucl  16371  funcres2b  16380  funcpropd  16383  xpcco1st  16647  xpccatid  16651  1stf1  16655  2ndf1  16658  1stfcl  16660  prf1  16663  prfcl  16666  prf1st  16667  prf2nd  16668  evlf1  16683  evlfcl  16685  curf1fval  16687  curf11  16689  curf1cl  16691  curfcl  16695  hof1fval  16716  txbas  21180  cnmpt1st  21281  txhmeo  21416  ptuncnv  21420  ptunhmeo  21421  xpstopnlem1  21422  xkohmeo  21428  prdstmdd  21737  ucnimalem  21894  fmucndlem  21905  fsum2cn  22482  ovoliunlem1  23077  lgsquadlem1  24905  lgsquadlem2  24906  usgrac  25880  edgss  25881  fimaproj  29228  eulerpartlemgs2  29769  cvmliftlem15  30534  msubty  30678  msubco  30682  msubvrs  30711  filnetlem4  31546  finixpnum  32564  poimirlem4  32583  poimirlem15  32594  poimirlem20  32599  poimirlem26  32605  poimirlem28  32607  heicant  32614  dicelvalN  35485  rmxypairf1o  36494  unxpwdom3  36683  fgraphxp  36808  elcnvlem  36926  dvnprodlem2  38837  etransclem46  39173  ovnsubaddlem1  39460  dmmpt2ssx2  41908
 Copyright terms: Public domain W3C validator