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

Step	Hyp	Ref	Expression
1		eqeq2 2775	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6561	. 2 ⊢ (𝐹:𝐶⟶onto𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6561	. 2 ⊢ (𝐹:𝐶⟶onto𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶onto𝐴 ↔ 𝐹:𝐶⟶onto𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5656   Fn wfn 6550  ⟶ontowfo 6553

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fo 6561

This theorem is used by:  fimadmfo  6824  f1oeq3  6833  foeq123d  6836  resdif  6865  ncanth  7395  ffoss  7979  rneqdmfinf1o  9347  fidomdm  9348  fifo  9448  brwdom  9585  brwdom2  9591  canthwdom  9597  ixpiunwdom  9608  fin1a2lem7  10508  dmct  10626  dmctOLD  10627  s7f1o  15145  znnen  16406  quslem  17741  znzrhfo  21880  rncmp  23741  connima  23770  conncn  23771  qtopcmplem  24053  qtoprest  24063  eupths  30828  pjhfo  32335  2ndresdjuf1o  33313  cycpmconjvlem  33769  algextdeglem8  34423  msrfo  36477  ivthALT  37300  bj-inftyexpitaufo  38314  poimirlem26  38755  poimirlem27  38756  opidon2OLD  38979  founiiun0  46408  focofob  48353  fundcmpsurinj  48694  fundcmpsurbijinj  48695  imasubc  50470  fullthinc  50788