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

Theorem foeq3 6351
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 2836 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 622 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 6129 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 6129 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1656  ran crn 5343   Fn wfn 6118  ontowfo 6121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-fo 6129
This theorem is referenced by:  fimadmfo  6362  f1oeq3  6369  foeq123d  6372  resdif  6398  ffoss  7389  rneqdmfinf1o  8511  fidomdm  8512  fifo  8607  brwdom  8741  brwdom2  8747  canthwdom  8753  ixpiunwdom  8765  fin1a2lem7  9543  dmct  9661  znnen  15315  quslem  16556  znzrhfo  20255  rncmp  21570  connima  21599  conncn  21600  qtopcmplem  21881  qtoprest  21891  eupths  27565  pjhfo  29109  msrfo  31978  ivthALT  32857  bj-inftyexpitaufo  33621  poimirlem26  33972  poimirlem27  33973  opidon2OLD  34188  founiiun0  40178
  Copyright terms: Public domain W3C validator