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

Theorem foeq3 5606
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
foeq3  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2442 . . 3  |-  ( A  =  B  ->  ( ran  F  =  A  <->  ran  F  =  B ) )
21anbi2d 696 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  =  A )  <->  ( F  Fn  C  /\  ran  F  =  B ) ) )
3 df-fo 5412 . 2  |-  ( F : C -onto-> A  <->  ( F  Fn  C  /\  ran  F  =  A ) )
4 df-fo 5412 . 2  |-  ( F : C -onto-> B  <->  ( F  Fn  C  /\  ran  F  =  B ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362   ran crn 4828    Fn wfn 5401   -onto->wfo 5404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-fo 5412
This theorem is referenced by:  f1oeq3  5622  foeq123d  5625  resdif  5649  ffoss  6527  fidomdm  7581  fifo  7670  brwdom  7770  brwdom2  7776  canthwdom  7782  ixpiunwdom  7794  fin1a2lem7  8563  znnen  13478  divslem  14464  znzrhfo  17822  rncmp  18841  conima  18871  concn  18872  qtopcmplem  19122  qtoprest  19132  opidon2  23634  pjhfo  24932  dmct  25838  ivthALT  28374
  Copyright terms: Public domain W3C validator