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

Theorem foelrn 5851
Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
Assertion
Ref Expression
foelrn  |-  ( ( F : A -onto-> B  /\  C  e.  B
)  ->  E. x  e.  A  C  =  ( F `  x ) )
Distinct variable groups:    x, F    x, A    x, B    x, C

Proof of Theorem foelrn
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dffo3 5847 . . 3  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  A. y  e.  B  E. x  e.  A  y  =  ( F `  x ) ) )
21simprbi 451 . 2  |-  ( F : A -onto-> B  ->  A. y  e.  B  E. x  e.  A  y  =  ( F `  x ) )
3 eqeq1 2414 . . . 4  |-  ( y  =  C  ->  (
y  =  ( F `
 x )  <->  C  =  ( F `  x ) ) )
43rexbidv 2691 . . 3  |-  ( y  =  C  ->  ( E. x  e.  A  y  =  ( F `  x )  <->  E. x  e.  A  C  =  ( F `  x ) ) )
54rspccva 3015 . 2  |-  ( ( A. y  e.  B  E. x  e.  A  y  =  ( F `  x )  /\  C  e.  B )  ->  E. x  e.  A  C  =  ( F `  x ) )
62, 5sylan 458 1  |-  ( ( F : A -onto-> B  /\  C  e.  B
)  ->  E. x  e.  A  C  =  ( F `  x ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2670   E.wrex 2671   -->wf 5413   -onto->wfo 5415   ` cfv 5417
This theorem is referenced by:  foco2  5852  fofinf1o  7350  fodomacn  7897  iunfictbso  7955  cff1  8098  cofsmo  8109  axcclem  8297  konigthlem  8403  tskuni  8618  fulli  14069  efgredlemc  15336  efgrelexlemb  15341  efgredeu  15343  ghmcyg  15464  znfld  16800  znrrg  16805  cygznlem3  16809  ovoliunnul  19360  lgsdchr  21089  ghgrplem1  21911  iunrdx  23971  crngohomfo  26510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-fo 5423  df-fv 5425
  Copyright terms: Public domain W3C validator