Theorem foeq3 6743

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 2747	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6497	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6497	. 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 5624   Fn wfn 6486  –onto→wfo 6489

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 2707

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

This theorem is referenced by:  fimadmfo  6754  f1oeq3  6763  foeq123d  6766  resdif  6794  ncanth  7313  ffoss  7890  rneqdmfinf1o  9235  fidomdm  9236  fifo  9337  brwdom  9474  brwdom2  9480  canthwdom  9486  ixpiunwdom  9497  fin1a2lem7  10318  dmct  10436  s7f1o  14891  znnen  16139  quslem  17466  znzrhfo  21504  rncmp  23342  connima  23371  conncn  23372  qtopcmplem  23653  qtoprest  23663  eupths  30256  pjhfo  31762  2ndresdjuf1o  32708  cycpmconjvlem  33202  algextdeglem8  33860  msrfo  35719  ivthALT  36508  bj-inftyexpitaufo  37376  poimirlem26  37816  poimirlem27  37817  opidon2OLD  38024  founiiun0  45471  focofob  47363  fundcmpsurinj  47692  fundcmpsurbijinj  47693  imasubc  49433  fullthinc  49732