Theorem foeq3 6670

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ran crn 5581   Fn wfn 6413  –onto→wfo 6416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fo 6424

This theorem is referenced by:  fimadmfo  6681  f1oeq3  6690  foeq123d  6693  resdif  6720  ncanth  7210  ffoss  7762  rneqdmfinf1o  9025  fidomdm  9026  fifo  9121  brwdom  9256  brwdom2  9262  canthwdom  9268  ixpiunwdom  9279  fin1a2lem7  10093  dmct  10211  znnen  15849  quslem  17171  znzrhfo  20667  rncmp  22455  connima  22484  conncn  22485  qtopcmplem  22766  qtoprest  22776  eupths  28465  pjhfo  29969  2ndresdjuf1o  30888  cycpmconjvlem  31310  msrfo  33408  ivthALT  34451  bj-inftyexpitaufo  35300  poimirlem26  35730  poimirlem27  35731  opidon2OLD  35939  founiiun0  42617  focofob  44459  fundcmpsurinj  44749  fundcmpsurbijinj  44750  fullthinc  46215