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

Theorem foeq3 6151
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 2662 . . 3 (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
21anbi2d 740 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3 df-fo 5932 . 2 (𝐹:𝐶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4 df-fo 5932 . 2 (𝐹:𝐶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  ran crn 5144   Fn wfn 5921  ontowfo 5924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fo 5932
This theorem is referenced by:  f1oeq3  6167  foeq123d  6170  resdif  6195  ffoss  7169  rneqdmfinf1o  8283  fidomdm  8284  fifo  8379  brwdom  8513  brwdom2  8519  canthwdom  8525  ixpiunwdom  8537  fin1a2lem7  9266  dmct  9384  znnen  14985  quslem  16250  znzrhfo  19944  rncmp  21247  connima  21276  conncn  21277  qtopcmplem  21558  qtoprest  21568  eupths  27178  pjhfo  28693  msrfo  31569  ivthALT  32455  poimirlem26  33565  poimirlem27  33566  opidon2OLD  33783  founiiun0  39691
  Copyright terms: Public domain W3C validator