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

Theorem foeq3 6819
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
foeq3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2747 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6569 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6569 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  ran crn 5690   Fn wfn 6558  ontowfo 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fo 6569
This theorem is referenced by:  fimadmfo  6830  f1oeq3  6839  foeq123d  6842  resdif  6870  ncanth  7386  ffoss  7969  rneqdmfinf1o  9371  fidomdm  9372  fifo  9470  brwdom  9605  brwdom2  9611  canthwdom  9617  ixpiunwdom  9628  fin1a2lem7  10444  dmct  10562  s7f1o  15002  znnen  16245  quslem  17590  znzrhfo  21584  rncmp  23420  connima  23449  conncn  23450  qtopcmplem  23731  qtoprest  23741  eupths  30229  pjhfo  31735  2ndresdjuf1o  32667  cycpmconjvlem  33144  algextdeglem8  33730  msrfo  35531  ivthALT  36318  bj-inftyexpitaufo  37185  poimirlem26  37633  poimirlem27  37634  opidon2OLD  37841  founiiun0  45133  focofob  47030  fundcmpsurinj  47334  fundcmpsurbijinj  47335  fullthinc  48846
  Copyright terms: Public domain W3C validator