Theorem foeq3 6817

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539  ran crn 5685   Fn wfn 6555  –onto→wfo 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-fo 6566

This theorem is referenced by:  fimadmfo  6828  f1oeq3  6837  foeq123d  6840  resdif  6868  ncanth  7387  ffoss  7971  rneqdmfinf1o  9374  fidomdm  9375  fifo  9473  brwdom  9608  brwdom2  9614  canthwdom  9620  ixpiunwdom  9631  fin1a2lem7  10447  dmct  10565  s7f1o  15006  znnen  16249  quslem  17589  znzrhfo  21567  rncmp  23405  connima  23434  conncn  23435  qtopcmplem  23716  qtoprest  23726  eupths  30220  pjhfo  31726  2ndresdjuf1o  32661  cycpmconjvlem  33162  algextdeglem8  33766  msrfo  35552  ivthALT  36337  bj-inftyexpitaufo  37204  poimirlem26  37654  poimirlem27  37655  opidon2OLD  37862  founiiun0  45200  focofob  47097  fundcmpsurinj  47401  fundcmpsurbijinj  47402  fullthinc  49124