Theorem foeq3 6563

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5520   Fn wfn 6319  –onto→wfo 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fo 6330

This theorem is referenced by:  fimadmfo  6574  f1oeq3  6581  foeq123d  6584  resdif  6610  ncanth  7091  ffoss  7629  rneqdmfinf1o  8784  fidomdm  8785  fifo  8880  brwdom  9015  brwdom2  9021  canthwdom  9027  ixpiunwdom  9038  fin1a2lem7  9817  dmct  9935  znnen  15557  quslem  16808  znzrhfo  20239  rncmp  22001  connima  22030  conncn  22031  qtopcmplem  22312  qtoprest  22322  eupths  27985  pjhfo  29489  2ndresdjuf1o  30412  cycpmconjvlem  30833  msrfo  32906  ivthALT  33796  bj-inftyexpitaufo  34617  poimirlem26  35083  poimirlem27  35084  opidon2OLD  35292  founiiun0  41817  fundcmpsurinj  43926  fundcmpsurbijinj  43927