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

Theorem foeq3 6075
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 2632 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 739 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 5858 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 5858 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  ran crn 5080   Fn wfn 5847  ontowfo 5850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-fo 5858
This theorem is referenced by:  f1oeq3  6091  foeq123d  6094  resdif  6119  ffoss  7081  rneqdmfinf1o  8194  fidomdm  8195  fifo  8290  brwdom  8424  brwdom2  8430  canthwdom  8436  ixpiunwdom  8448  fin1a2lem7  9180  dmct  9298  znnen  14877  quslem  16135  znzrhfo  19828  rncmp  21122  connima  21151  conncn  21152  qtopcmplem  21433  qtoprest  21443  eupths  26943  pjhfo  28435  msrfo  31186  ivthALT  32007  poimirlem26  33102  poimirlem27  33103  opidon2OLD  33320  founiiun0  38882
  Copyright terms: Public domain W3C validator