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

Theorem foeq2 6566
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 6419 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 632 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3 df-fo 6334 . 2 (𝐹:𝐴onto𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4 df-fo 6334 . 2 (𝐹:𝐵onto𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))
52, 3, 43bitr4g 317 1 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  ran crn 5524   Fn wfn 6323  ontowfo 6326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-fn 6331  df-fo 6334
This theorem is referenced by:  f1oeq2  6584  foeq123d  6588  tposfo  7906  brwdom  9019  brwdom2  9025  canthwdom  9031  cfslb2n  9683  0ramcl  16353  ghmcyg  19013  txcmpb  22253  qtoptopon  22313  fsupprnfi  30456  opidon2OLD  35291
  Copyright terms: Public domain W3C validator