Theorem foeq3 6754

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5635   Fn wfn 6497  –onto→wfo 6500

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fo 6508

This theorem is referenced by:  fimadmfo  6765  f1oeq3  6774  foeq123d  6777  resdif  6805  ncanth  7325  ffoss  7902  rneqdmfinf1o  9247  fidomdm  9248  fifo  9349  brwdom  9486  brwdom2  9492  canthwdom  9498  ixpiunwdom  9509  fin1a2lem7  10330  dmct  10448  s7f1o  14903  znnen  16151  quslem  17478  znzrhfo  21519  rncmp  23357  connima  23386  conncn  23387  qtopcmplem  23668  qtoprest  23678  eupths  30293  pjhfo  31800  2ndresdjuf1o  32746  cycpmconjvlem  33241  algextdeglem8  33908  msrfo  35768  ivthALT  36557  bj-inftyexpitaufo  37484  poimirlem26  37926  poimirlem27  37927  opidon2OLD  38134  founiiun0  45578  focofob  47469  fundcmpsurinj  47798  fundcmpsurbijinj  47799  imasubc  49539  fullthinc  49838