Theorem foeq3 6813

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534  ran crn 5683   Fn wfn 6549  –onto→wfo 6552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-fo 6560

This theorem is referenced by:  fimadmfo  6824  f1oeq3  6833  foeq123d  6836  resdif  6864  ncanth  7378  ffoss  7959  rneqdmfinf1o  9375  fidomdm  9376  fifo  9475  brwdom  9610  brwdom2  9616  canthwdom  9622  ixpiunwdom  9633  fin1a2lem7  10449  dmct  10567  znnen  16214  quslem  17558  znzrhfo  21545  rncmp  23391  connima  23420  conncn  23421  qtopcmplem  23702  qtoprest  23712  eupths  30133  pjhfo  31639  2ndresdjuf1o  32567  cycpmconjvlem  33019  algextdeglem8  33591  msrfo  35374  ivthALT  36047  bj-inftyexpitaufo  36909  poimirlem26  37347  poimirlem27  37348  opidon2OLD  37555  founiiun0  44797  focofob  46693  fundcmpsurinj  46981  fundcmpsurbijinj  46982  fullthinc  48367