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

Theorem op1std 6792
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 5853 . 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 6790 . 2  |-  ( 1st `  <. A ,  B >. )  =  A
51, 4syl6eq 2498 1  |-  ( C  =  <. A ,  B >.  ->  ( 1st `  C
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802   _Vcvv 3093   <.cop 4017   ` cfv 5575   1stc1st 6780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-iota 5538  df-fun 5577  df-fv 5583  df-1st 6782
This theorem is referenced by:  1st2val  6808  xp1st  6812  sbcopeq1a  6834  csbopeq1a  6835  eloprabi  6844  mpt2mptsx  6845  dmmpt2ssx  6847  fmpt2x  6848  ovmptss  6863  fmpt2co  6865  df1st2  6868  fsplit  6887  frxp  6892  xporderlem  6893  fnwelem  6897  xpf1o  7678  mapunen  7685  xpwdomg  8011  hsmexlem2  8807  fsumcom2  13565  qredeu  14122  isfuncd  15105  cofucl  15128  funcres2b  15137  funcpropd  15140  xpcco1st  15324  xpccatid  15328  1stf1  15332  2ndf1  15335  1stfcl  15337  prf1  15340  prfcl  15343  prf1st  15344  prf2nd  15345  evlf1  15360  evlfcl  15362  curf1fval  15364  curf11  15366  curf1cl  15368  curfcl  15372  hof1fval  15393  txbas  19938  cnmpt1st  20039  txhmeo  20174  ptuncnv  20178  ptunhmeo  20179  xpstopnlem1  20180  xkohmeo  20186  prdstmdd  20492  ucnimalem  20653  fmucndlem  20664  fsum2cn  21245  ovoliunlem1  21783  lgsquadlem1  23498  lgsquadlem2  23499  usgrac  24220  edgss  24221  fimaproj  27706  eulerpartlemgs2  28189  cvmliftlem15  28613  msubty  28757  msubco  28761  msubvrs  28790  fprodcom2  29086  finixpnum  30010  heicant  30021  filnetlem4  30171  rmxypairf1o  30819  unxpwdom3  31013  fgraphxp  31144  dmmpt2ssx2  32654  dicelvalN  36628
  Copyright terms: Public domain W3C validator