Theorem foeq3 6026

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ran crn 5039   Fn wfn 5799  –onto→wfo 5802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fo 5810

This theorem is referenced by:  f1oeq3  6042  foeq123d  6045  resdif  6070  ffoss  7020  rneqdmfinf1o  8127  fidomdm  8128  fifo  8221  brwdom  8355  brwdom2  8361  canthwdom  8367  ixpiunwdom  8379  fin1a2lem7  9111  znnen  14780  quslem  16026  znzrhfo  19715  rncmp  21009  conima  21038  concn  21039  qtopcmplem  21320  qtoprest  21330  pjhfo  27949  dmct  28877  msrfo  30697  ivthALT  31500  poimirlem26  32605  poimirlem27  32606  opidon2OLD  32823  founiiun0  38372