Theorem foeq3 6678

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 6432	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6432	. 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 5585   Fn wfn 6421  –onto→wfo 6424

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 6432

This theorem is referenced by:  fimadmfo  6689  f1oeq3  6698  foeq123d  6701  resdif  6729  ncanth  7222  ffoss  7778  rneqdmfinf1o  9082  fidomdm  9083  fifo  9178  brwdom  9313  brwdom2  9319  canthwdom  9325  ixpiunwdom  9336  fin1a2lem7  10172  dmct  10290  znnen  15931  quslem  17264  znzrhfo  20765  rncmp  22557  connima  22586  conncn  22587  qtopcmplem  22868  qtoprest  22878  eupths  28572  pjhfo  30076  2ndresdjuf1o  30995  cycpmconjvlem  31416  msrfo  33516  ivthALT  34532  bj-inftyexpitaufo  35381  poimirlem26  35811  poimirlem27  35812  opidon2OLD  36020  founiiun0  42709  focofob  44550  fundcmpsurinj  44839  fundcmpsurbijinj  44840  fullthinc  46305