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

Theorem foeq2 6803
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 6642 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3 df-fo 6550 . 2 (𝐹:𝐴onto𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4 df-fo 6550 . 2 (𝐹:𝐵onto𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  ran crn 5678   Fn wfn 6539  ontowfo 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547  df-fo 6550
This theorem is referenced by:  foco  6820  f1oeq2  6823  foeq123d  6827  tposfo  8238  brwdom  9562  brwdom2  9568  canthwdom  9574  cfslb2n  10263  0ramcl  16956  ghmcyg  19764  txcmpb  23148  qtoptopon  23208  fsupprnfi  31914  opidon2OLD  36722  fnfocofob  45787  fullthinc  47666
  Copyright terms: Public domain W3C validator