Theorem foeq3 6778

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562  ran crn 5650   Fn wfn 6518  –onto→wfo 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-fo 6529

This theorem is referenced by:  fimadmfo  6789  f1oeq3  6798  foeq123d  6801  resdif  6830  ncanth  7353  ffoss  7929  rneqdmfinf1o  9278  fidomdm  9279  fifo  9380  brwdom  9517  brwdom2  9523  canthwdom  9529  ixpiunwdom  9540  fin1a2lem7  10365  dmct  10483  s7f1o  14981  znnen  16246  quslem  17575  znzrhfo  21601  rncmp  23458  connima  23487  conncn  23488  qtopcmplem  23769  qtoprest  23779  eupths  30404  pjhfo  31911  2ndresdjuf1o  32854  cycpmconjvlem  33323  algextdeglem8  34023  msrfo  35901  ivthALT  36700  bj-inftyexpitaufo  37699  poimirlem26  38150  poimirlem27  38151  opidon2OLD  38358  founiiun0  45773  focofob  47679  fundcmpsurinj  48020  fundcmpsurbijinj  48021  imasubc  49777  fullthinc  50076