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

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

Proof of Theorem foeq2
StepHypRef Expression
1 fneq2 5894 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 737 . 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-fn 5807  df-fo 5810 This theorem is referenced by:  f1oeq2  6041  foeq123d  6045  tposfo  7266  brwdom  8355  brwdom2  8361  canthwdom  8367  cfslb2n  8973  fodomg  9228  0ramcl  15565  ghmcyg  18120  txcmpb  21257  qtoptopon  21317  opidon2OLD  32823
 Copyright terms: Public domain W3C validator