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

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

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2748 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6566 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6566 . 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 1539  ran crn 5685   Fn wfn 6555  ontowfo 6558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-fo 6566
This theorem is referenced by:  fimadmfo  6828  f1oeq3  6837  foeq123d  6840  resdif  6868  ncanth  7387  ffoss  7971  rneqdmfinf1o  9374  fidomdm  9375  fifo  9473  brwdom  9608  brwdom2  9614  canthwdom  9620  ixpiunwdom  9631  fin1a2lem7  10447  dmct  10565  s7f1o  15006  znnen  16249  quslem  17589  znzrhfo  21567  rncmp  23405  connima  23434  conncn  23435  qtopcmplem  23716  qtoprest  23726  eupths  30220  pjhfo  31726  2ndresdjuf1o  32661  cycpmconjvlem  33162  algextdeglem8  33766  msrfo  35552  ivthALT  36337  bj-inftyexpitaufo  37204  poimirlem26  37654  poimirlem27  37655  opidon2OLD  37862  founiiun0  45200  focofob  47097  fundcmpsurinj  47401  fundcmpsurbijinj  47402  fullthinc  49124
  Copyright terms: Public domain W3C validator