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

Theorem foeq1 6750
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 6591 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5890 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32eqeq1d 2738 . . 3 (𝐹 = 𝐺 → (ran 𝐹 = 𝐵 ↔ ran 𝐺 = 𝐵))
41, 3anbi12d 631 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵)))
5 df-fo 6500 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6 df-fo 6500 . 2 (𝐺:𝐴onto𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵))
74, 5, 63bitr4g 313 1 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  ran crn 5633   Fn wfn 6489  ontowfo 6492
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6496  df-fn 6497  df-fo 6500
This theorem is referenced by:  fimadmfoALT  6765  f1oeq1  6770  foeq123d  6775  resdif  6803  exfo  7052  mapfoss  8787  fodomr  9069  dif1enlem  9097  dif1enlemOLD  9098  fowdom  9504  brwdom2  9506  canthp1lem2  10586  mndfo  18577  sursubmefmnd  18703  znzrhfo  20950  pjhfo  30546  elunop  30712  elunop2  30853  symgcom  31829  nnfoctbdjlem  44666  fcoreslem3  45269  fcoresfo  45275  fcoresfob  45276  fundcmpsurbijinjpreimafv  45569
  Copyright terms: Public domain W3C validator