Theorem foeq3 6752

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5632   Fn wfn 6494  –onto→wfo 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fo 6505

This theorem is referenced by:  fimadmfo  6763  f1oeq3  6772  foeq123d  6775  resdif  6803  ncanth  7324  ffoss  7904  rneqdmfinf1o  9260  fidomdm  9261  fifo  9359  brwdom  9496  brwdom2  9502  canthwdom  9508  ixpiunwdom  9519  fin1a2lem7  10335  dmct  10453  s7f1o  14908  znnen  16156  quslem  17482  znzrhfo  21489  rncmp  23316  connima  23345  conncn  23346  qtopcmplem  23627  qtoprest  23637  eupths  30179  pjhfo  31685  2ndresdjuf1o  32624  cycpmconjvlem  33113  algextdeglem8  33707  msrfo  35526  ivthALT  36316  bj-inftyexpitaufo  37183  poimirlem26  37633  poimirlem27  37634  opidon2OLD  37841  founiiun0  45177  focofob  47074  fundcmpsurinj  47403  fundcmpsurbijinj  47404  imasubc  49133  fullthinc  49432