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

Theorem op1std 7046
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 6087 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (1st𝐶) = (1st ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op1st 7044 . 2 (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
51, 4syl6eq 2659 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (1st𝐶) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  Vcvv 3172  cop 4130  cfv 5789  1st c1st 7034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-iota 5753  df-fun 5791  df-fv 5797  df-1st 7036
This theorem is referenced by:  1st2val  7062  xp1st  7066  sbcopeq1a  7088  csbopeq1a  7089  eloprabi  7098  mpt2mptsx  7099  dmmpt2ssx  7101  fmpt2x  7102  ovmptss  7122  fmpt2co  7124  df1st2  7127  fsplit  7146  frxp  7151  xporderlem  7152  fnwelem  7156  xpf1o  7984  mapunen  7991  xpwdomg  8350  hsmexlem2  9109  fsumcom2  14295  fsumcom2OLD  14296  fprodcom2  14501  fprodcom2OLD  14502  qredeu  15158  isfuncd  16296  cofucl  16319  funcres2b  16328  funcpropd  16331  xpcco1st  16595  xpccatid  16599  1stf1  16603  2ndf1  16606  1stfcl  16608  prf1  16611  prfcl  16614  prf1st  16615  prf2nd  16616  evlf1  16631  evlfcl  16633  curf1fval  16635  curf11  16637  curf1cl  16639  curfcl  16643  hof1fval  16664  txbas  21127  cnmpt1st  21228  txhmeo  21363  ptuncnv  21367  ptunhmeo  21368  xpstopnlem1  21369  xkohmeo  21375  prdstmdd  21684  ucnimalem  21841  fmucndlem  21852  fsum2cn  22429  ovoliunlem1  23021  lgsquadlem1  24849  lgsquadlem2  24850  usgrac  25673  edgss  25674  fimaproj  29021  eulerpartlemgs2  29562  cvmliftlem15  30327  msubty  30471  msubco  30475  msubvrs  30504  filnetlem4  31339  finixpnum  32347  poimirlem4  32366  poimirlem15  32377  poimirlem20  32382  poimirlem26  32388  poimirlem28  32390  heicant  32397  dicelvalN  35268  rmxypairf1o  36277  unxpwdom3  36466  fgraphxp  36591  elcnvlem  36709  dvnprodlem2  38620  etransclem46  38956  ovnsubaddlem1  39243  dmmpt2ssx2  41889
  Copyright terms: Public domain W3C validator