Theorem foeq3 6734

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 2741	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6488	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6488	. 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 5620   Fn wfn 6477  –onto→wfo 6480

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 2701

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

This theorem is referenced by:  fimadmfo  6745  f1oeq3  6754  foeq123d  6757  resdif  6785  ncanth  7304  ffoss  7881  rneqdmfinf1o  9223  fidomdm  9224  fifo  9322  brwdom  9459  brwdom2  9465  canthwdom  9471  ixpiunwdom  9482  fin1a2lem7  10300  dmct  10418  s7f1o  14873  znnen  16121  quslem  17447  znzrhfo  21454  rncmp  23281  connima  23310  conncn  23311  qtopcmplem  23592  qtoprest  23602  eupths  30148  pjhfo  31654  2ndresdjuf1o  32601  cycpmconjvlem  33092  algextdeglem8  33707  msrfo  35539  ivthALT  36329  bj-inftyexpitaufo  37196  poimirlem26  37646  poimirlem27  37647  opidon2OLD  37854  founiiun0  45188  focofob  47084  fundcmpsurinj  47413  fundcmpsurbijinj  47414  imasubc  49156  fullthinc  49455