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

Theorem foeq3 6329
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 2810 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 623 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6107 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6107 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  ran crn 5313   Fn wfn 6096  ontowfo 6099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2792  df-fo 6107
This theorem is referenced by:  fimadmfo  6340  f1oeq3  6347  foeq123d  6350  resdif  6376  ffoss  7362  rneqdmfinf1o  8484  fidomdm  8485  fifo  8580  brwdom  8714  brwdom2  8720  canthwdom  8726  ixpiunwdom  8738  fin1a2lem7  9516  dmct  9634  znnen  15277  quslem  16518  znzrhfo  20217  rncmp  21528  connima  21557  conncn  21558  qtopcmplem  21839  qtoprest  21849  eupths  27544  pjhfo  29090  msrfo  31960  ivthALT  32842  poimirlem26  33924  poimirlem27  33925  opidon2OLD  34140  founiiun0  40131
  Copyright terms: Public domain W3C validator