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

Theorem op1std 6727
Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
op1st.1  |-  A  e. 
_V
op1st.2  |-  B  e. 
_V
Assertion
Ref Expression
op1std  |-  ( C  =  <. A ,  B >.  ->  ( 1st `  C
)  =  A )

Proof of Theorem op1std
StepHypRef Expression
1 fveq2 5787 . 2  |-  ( C  =  <. A ,  B >.  ->  ( 1st `  C
)  =  ( 1st `  <. A ,  B >. ) )
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op1st 6725 . 2  |-  ( 1st `  <. A ,  B >. )  =  A
51, 4syl6eq 2449 1  |-  ( C  =  <. A ,  B >.  ->  ( 1st `  C
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1836   _Vcvv 3047   <.cop 3963   ` cfv 5509   1stc1st 6715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-iota 5473  df-fun 5511  df-fv 5517  df-1st 6717
This theorem is referenced by:  1st2val  6743  xp1st  6747  sbcopeq1a  6769  csbopeq1a  6770  eloprabi  6779  mpt2mptsx  6780  dmmpt2ssx  6782  fmpt2x  6783  ovmptss  6798  fmpt2co  6800  df1st2  6803  fsplit  6822  frxp  6827  xporderlem  6828  fnwelem  6832  xpf1o  7616  mapunen  7623  xpwdomg  7944  hsmexlem2  8738  fsumcom2  13610  fprodcom2  13809  qredeu  14269  isfuncd  15290  cofucl  15313  funcres2b  15322  funcpropd  15325  xpcco1st  15589  xpccatid  15593  1stf1  15597  2ndf1  15600  1stfcl  15602  prf1  15605  prfcl  15608  prf1st  15609  prf2nd  15610  evlf1  15625  evlfcl  15627  curf1fval  15629  curf11  15631  curf1cl  15633  curfcl  15637  hof1fval  15658  txbas  20172  cnmpt1st  20273  txhmeo  20408  ptuncnv  20412  ptunhmeo  20413  xpstopnlem1  20414  xkohmeo  20420  prdstmdd  20726  ucnimalem  20887  fmucndlem  20898  fsum2cn  21479  ovoliunlem1  22017  lgsquadlem1  23765  lgsquadlem2  23766  usgrac  24493  edgss  24494  fimaproj  28021  eulerpartlemgs2  28538  cvmliftlem15  28968  msubty  29112  msubco  29116  msubvrs  29145  finixpnum  30239  heicant  30250  filnetlem4  30401  rmxypairf1o  31048  unxpwdom3  31243  fgraphxp  31375  dvnprodlem2  31945  etransclem46  32264  dmmpt2ssx2  33161  dicelvalN  37353
  Copyright terms: Public domain W3C validator