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

Theorem foeq3 6813
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 2738 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 628 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6560 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6560 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 313 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  ran crn 5683   Fn wfn 6549  ontowfo 6552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-fo 6560
This theorem is referenced by:  fimadmfo  6824  f1oeq3  6833  foeq123d  6836  resdif  6864  ncanth  7378  ffoss  7959  rneqdmfinf1o  9375  fidomdm  9376  fifo  9475  brwdom  9610  brwdom2  9616  canthwdom  9622  ixpiunwdom  9633  fin1a2lem7  10449  dmct  10567  znnen  16214  quslem  17558  znzrhfo  21545  rncmp  23391  connima  23420  conncn  23421  qtopcmplem  23702  qtoprest  23712  eupths  30133  pjhfo  31639  2ndresdjuf1o  32567  cycpmconjvlem  33019  algextdeglem8  33591  msrfo  35374  ivthALT  36047  bj-inftyexpitaufo  36909  poimirlem26  37347  poimirlem27  37348  opidon2OLD  37555  founiiun0  44797  focofob  46693  fundcmpsurinj  46981  fundcmpsurbijinj  46982  fullthinc  48367
  Copyright terms: Public domain W3C validator