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

Theorem foeq3 6754
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 629 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6502 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6502 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 313 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  ran crn 5634   Fn wfn 6491  ontowfo 6494
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-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-fo 6502
This theorem is referenced by:  fimadmfo  6765  f1oeq3  6774  foeq123d  6777  resdif  6805  ncanth  7311  ffoss  7878  rneqdmfinf1o  9272  fidomdm  9273  fifo  9368  brwdom  9503  brwdom2  9509  canthwdom  9515  ixpiunwdom  9526  fin1a2lem7  10342  dmct  10460  znnen  16094  quslem  17425  znzrhfo  20954  rncmp  22747  connima  22776  conncn  22777  qtopcmplem  23058  qtoprest  23068  eupths  29144  pjhfo  30648  2ndresdjuf1o  31566  cycpmconjvlem  31990  msrfo  34140  ivthALT  34807  bj-inftyexpitaufo  35673  poimirlem26  36104  poimirlem27  36105  opidon2OLD  36313  founiiun0  43399  focofob  45302  fundcmpsurinj  45591  fundcmpsurbijinj  45592  fullthinc  47056
  Copyright terms: Public domain W3C validator