Theorem foeq2 6741

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5623   Fn wfn 6485  –onto→wfo 6488

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6493  df-fo 6496

This theorem is referenced by:  foco  6758  f1oeq2  6761  foeq123d  6765  tposfo  8194  brwdom  9473  brwdom2  9479  canthwdom  9485  cfslb2n  10179  0ramcl  16983  ghmcyg  19860  txcmpb  23618  qtoptopon  23678  fsupprnfi  32785  opidon2OLD  38186  fnfocofob  47524  fullthinc  49922