Theorem foeq2 6740

Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
foeq2	⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))

Proof of Theorem foeq2

Step	Hyp	Ref	Expression
1		fneq2 6581	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
2	1	anbi1d 638	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3		df-fo 6495	. 2 ⊢ (𝐹:𝐴–onto→𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4		df-fo 6495	. 2 ⊢ (𝐹:𝐵–onto→𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))
5	2, 3, 4	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ran crn 5622   Fn wfn 6484  –onto→wfo 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-fn 6492  df-fo 6495

This theorem is referenced by:  foco  6757  f1oeq2  6760  foeq123d  6764  tposfo  8197  brwdom  9476  brwdom2  9482  canthwdom  9488  cfslb2n  10185  0ramcl  16989  ghmcyg  19866  txcmpb  23631  qtoptopon  23691  fsupprnfi  32788  opidon2OLD  38236  fnfocofob  47556  fullthinc  49954