Theorem foeq3 6804

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539  ran crn 5678   Fn wfn 6539  –onto→wfo 6542

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-fo 6550

This theorem is referenced by:  fimadmfo  6815  f1oeq3  6824  foeq123d  6827  resdif  6855  ncanth  7367  ffoss  7936  rneqdmfinf1o  9332  fidomdm  9333  fifo  9431  brwdom  9566  brwdom2  9572  canthwdom  9578  ixpiunwdom  9589  fin1a2lem7  10405  dmct  10523  znnen  16161  quslem  17495  znzrhfo  21324  rncmp  23122  connima  23151  conncn  23152  qtopcmplem  23433  qtoprest  23443  eupths  29718  pjhfo  31224  2ndresdjuf1o  32140  cycpmconjvlem  32568  algextdeglem8  33067  msrfo  34833  ivthALT  35525  bj-inftyexpitaufo  36388  poimirlem26  36819  poimirlem27  36820  opidon2OLD  37027  founiiun0  44189  focofob  46088  fundcmpsurinj  46377  fundcmpsurbijinj  46378  fullthinc  47755