Theorem foeq3 6793

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5660   Fn wfn 6531  –onto→wfo 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-fo 6542

This theorem is referenced by:  fimadmfo  6804  f1oeq3  6813  foeq123d  6816  resdif  6844  ncanth  7365  ffoss  7949  rneqdmfinf1o  9350  fidomdm  9351  fifo  9449  brwdom  9586  brwdom2  9592  canthwdom  9598  ixpiunwdom  9609  fin1a2lem7  10425  dmct  10543  s7f1o  14990  znnen  16235  quslem  17562  znzrhfo  21513  rncmp  23339  connima  23368  conncn  23369  qtopcmplem  23650  qtoprest  23660  eupths  30186  pjhfo  31692  2ndresdjuf1o  32633  cycpmconjvlem  33157  algextdeglem8  33763  msrfo  35573  ivthALT  36358  bj-inftyexpitaufo  37225  poimirlem26  37675  poimirlem27  37676  opidon2OLD  37883  founiiun0  45181  focofob  47076  fundcmpsurinj  47390  fundcmpsurbijinj  47391  imasubc  49058  fullthinc  49303