Theorem foeq3 6803

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ran crn 5677   Fn wfn 6538  –onto→wfo 6541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fo 6549

This theorem is referenced by:  fimadmfo  6814  f1oeq3  6823  foeq123d  6826  resdif  6854  ncanth  7362  ffoss  7931  rneqdmfinf1o  9327  fidomdm  9328  fifo  9426  brwdom  9561  brwdom2  9567  canthwdom  9573  ixpiunwdom  9584  fin1a2lem7  10400  dmct  10518  znnen  16154  quslem  17488  znzrhfo  21102  rncmp  22899  connima  22928  conncn  22929  qtopcmplem  23210  qtoprest  23220  eupths  29450  pjhfo  30954  2ndresdjuf1o  31870  cycpmconjvlem  32295  msrfo  34532  ivthALT  35215  bj-inftyexpitaufo  36078  poimirlem26  36509  poimirlem27  36510  opidon2OLD  36717  founiiun0  43878  focofob  45778  fundcmpsurinj  46067  fundcmpsurbijinj  46068  fullthinc  47656