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

Theorem foeq3 6026
 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 2621 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 736 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 5810 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 5810 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 302 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ran crn 5039   Fn wfn 5799  –onto→wfo 5802 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fo 5810 This theorem is referenced by:  f1oeq3  6042  foeq123d  6045  resdif  6070  ffoss  7020  rneqdmfinf1o  8127  fidomdm  8128  fifo  8221  brwdom  8355  brwdom2  8361  canthwdom  8367  ixpiunwdom  8379  fin1a2lem7  9111  znnen  14780  quslem  16026  znzrhfo  19715  rncmp  21009  conima  21038  concn  21039  qtopcmplem  21320  qtoprest  21330  pjhfo  27949  dmct  28877  msrfo  30697  ivthALT  31500  poimirlem26  32605  poimirlem27  32606  opidon2OLD  32823  founiiun0  38372
 Copyright terms: Public domain W3C validator