Theorem foeq3 6750

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 2748	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6504	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6504	. 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 5632   Fn wfn 6493  –onto→wfo 6496

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fo 6504

This theorem is referenced by:  fimadmfo  6761  f1oeq3  6770  foeq123d  6773  resdif  6801  ncanth  7322  ffoss  7899  rneqdmfinf1o  9243  fidomdm  9244  fifo  9345  brwdom  9482  brwdom2  9488  canthwdom  9494  ixpiunwdom  9505  fin1a2lem7  10328  dmct  10446  s7f1o  14928  znnen  16179  quslem  17507  znzrhfo  21527  rncmp  23361  connima  23390  conncn  23391  qtopcmplem  23672  qtoprest  23682  eupths  30270  pjhfo  31777  2ndresdjuf1o  32723  cycpmconjvlem  33202  algextdeglem8  33868  msrfo  35728  ivthALT  36517  bj-inftyexpitaufo  37516  poimirlem26  37967  poimirlem27  37968  opidon2OLD  38175  founiiun0  45620  focofob  47528  fundcmpsurinj  47869  fundcmpsurbijinj  47870  imasubc  49626  fullthinc  49925