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

Theorem foeq2 6265
 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 6133 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 743 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3 df-fo 6047 . 2 (𝐹:𝐴onto𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4 df-fo 6047 . 2 (𝐹:𝐵onto𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1624  ran crn 5259   Fn wfn 6036  –onto→wfo 6039 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745  df-fn 6044  df-fo 6047 This theorem is referenced by:  f1oeq2  6281  foeq123d  6285  tposfo  7540  brwdom  8629  brwdom2  8635  canthwdom  8641  cfslb2n  9274  fodomg  9529  0ramcl  15921  ghmcyg  18489  txcmpb  21641  qtoptopon  21701  opidon2OLD  33958
 Copyright terms: Public domain W3C validator