Theorem foeq3 6733

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ran crn 5615   Fn wfn 6476  –onto→wfo 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fo 6487

This theorem is referenced by:  fimadmfo  6744  f1oeq3  6753  foeq123d  6756  resdif  6784  ncanth  7301  ffoss  7878  rneqdmfinf1o  9217  fidomdm  9218  fifo  9316  brwdom  9453  brwdom2  9459  canthwdom  9465  ixpiunwdom  9476  fin1a2lem7  10297  dmct  10415  s7f1o  14873  znnen  16121  quslem  17447  znzrhfo  21484  rncmp  23311  connima  23340  conncn  23341  qtopcmplem  23622  qtoprest  23632  eupths  30180  pjhfo  31686  2ndresdjuf1o  32632  cycpmconjvlem  33110  algextdeglem8  33737  msrfo  35590  ivthALT  36379  bj-inftyexpitaufo  37246  poimirlem26  37685  poimirlem27  37686  opidon2OLD  37893  founiiun0  45286  focofob  47179  fundcmpsurinj  47508  fundcmpsurbijinj  47509  imasubc  49251  fullthinc  49550