Theorem foeq3 6686

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ran crn 5590   Fn wfn 6428  –onto→wfo 6431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fo 6439

This theorem is referenced by:  fimadmfo  6697  f1oeq3  6706  foeq123d  6709  resdif  6737  ncanth  7230  ffoss  7788  rneqdmfinf1o  9095  fidomdm  9096  fifo  9191  brwdom  9326  brwdom2  9332  canthwdom  9338  ixpiunwdom  9349  fin1a2lem7  10162  dmct  10280  znnen  15921  quslem  17254  znzrhfo  20755  rncmp  22547  connima  22576  conncn  22577  qtopcmplem  22858  qtoprest  22868  eupths  28564  pjhfo  30068  2ndresdjuf1o  30987  cycpmconjvlem  31408  msrfo  33508  ivthALT  34524  bj-inftyexpitaufo  35373  poimirlem26  35803  poimirlem27  35804  opidon2OLD  36012  founiiun0  42728  focofob  44572  fundcmpsurinj  44861  fundcmpsurbijinj  44862  fullthinc  46327