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

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

Proof of Theorem foeq1
StepHypRef Expression
1 fneq1 6430 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5782 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32eqeq1d 2760 . . 3 (𝐹 = 𝐺 → (ran 𝐹 = 𝐵 ↔ ran 𝐺 = 𝐵))
41, 3anbi12d 633 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵)))
5 df-fo 6346 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6 df-fo 6346 . 2 (𝐺:𝐴onto𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵))
74, 5, 63bitr4g 317 1 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5529   Fn wfn 6335  –onto→wfo 6338 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-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-fun 6342  df-fn 6343  df-fo 6346 This theorem is referenced by:  fimadmfoALT  6592  f1oeq1  6595  foeq123d  6600  resdif  6627  exfo  6868  mapfoss  8447  fodomr  8703  dif1enlem  8744  fowdom  9081  brwdom2  9083  canthp1lem2  10126  mndfo  18015  sursubmefmnd  18141  znzrhfo  20329  pjhfo  29602  elunop  29768  elunop2  29909  symgcom  30891  nnfoctbdjlem  43505  fundcmpsurbijinjpreimafv  44351
 Copyright terms: Public domain W3C validator