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

Theorem foeq3 6581
 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 2831 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6354 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6354 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 316 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1530  ran crn 5549   Fn wfn 6343  –onto→wfo 6346 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-fo 6354 This theorem is referenced by:  fimadmfo  6592  f1oeq3  6599  foeq123d  6602  resdif  6628  ncanth  7104  ffoss  7639  rneqdmfinf1o  8792  fidomdm  8793  fifo  8888  brwdom  9023  brwdom2  9029  canthwdom  9035  ixpiunwdom  9047  fin1a2lem7  9820  dmct  9938  znnen  15557  quslem  16808  znzrhfo  20686  rncmp  21996  connima  22025  conncn  22026  qtopcmplem  22307  qtoprest  22317  eupths  27971  pjhfo  29475  cycpmconjvlem  30776  msrfo  32781  ivthALT  33671  bj-inftyexpitaufo  34471  poimirlem26  34905  poimirlem27  34906  opidon2OLD  35119  founiiun0  41435  fundcmpsurinj  43554  fundcmpsurbijinj  43555
 Copyright terms: Public domain W3C validator