Theorem foeq3 6819

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 2747	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6569	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6569	. 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ran crn 5690   Fn wfn 6558  –onto→wfo 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fo 6569

This theorem is referenced by:  fimadmfo  6830  f1oeq3  6839  foeq123d  6842  resdif  6870  ncanth  7386  ffoss  7969  rneqdmfinf1o  9371  fidomdm  9372  fifo  9470  brwdom  9605  brwdom2  9611  canthwdom  9617  ixpiunwdom  9628  fin1a2lem7  10444  dmct  10562  s7f1o  15002  znnen  16245  quslem  17590  znzrhfo  21584  rncmp  23420  connima  23449  conncn  23450  qtopcmplem  23731  qtoprest  23741  eupths  30229  pjhfo  31735  2ndresdjuf1o  32667  cycpmconjvlem  33144  algextdeglem8  33730  msrfo  35531  ivthALT  36318  bj-inftyexpitaufo  37185  poimirlem26  37633  poimirlem27  37634  opidon2OLD  37841  founiiun0  45133  focofob  47030  fundcmpsurinj  47334  fundcmpsurbijinj  47335  fullthinc  48846