Theorem foeq2 6744

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 6585	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
2	1	anbi1d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)))
3		df-fo 6499	. 2 ⊢ (𝐹:𝐴–onto→𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶))
4		df-fo 6499	. 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 5626   Fn wfn 6488  –onto→wfo 6491

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 6496  df-fo 6499

This theorem is referenced by:  foco  6761  f1oeq2  6764  foeq123d  6768  tposfo  8197  brwdom  9476  brwdom2  9482  canthwdom  9488  cfslb2n  10182  0ramcl  16955  ghmcyg  19829  txcmpb  23592  qtoptopon  23652  fsupprnfi  32773  opidon2OLD  38057  fnfocofob  47392  fullthinc  49762