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

Theorem foeq2 6818
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 6661 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3 df-fo 6569 . 2 (𝐹:𝐴onto𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4 df-fo 6569 . 2 (𝐹:𝐵onto𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  ran crn 5690   Fn wfn 6558  ontowfo 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566  df-fo 6569
This theorem is referenced by:  foco  6835  f1oeq2  6838  foeq123d  6842  tposfo  8277  brwdom  9605  brwdom2  9611  canthwdom  9617  cfslb2n  10306  0ramcl  17057  ghmcyg  19929  txcmpb  23668  qtoptopon  23728  fsupprnfi  32707  opidon2OLD  37841  fnfocofob  47029  fullthinc  48846
  Copyright terms: Public domain W3C validator