Theorem foeq3 6741

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ran crn 5622   Fn wfn 6484  –onto→wfo 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-fo 6495

This theorem is referenced by:  fimadmfo  6752  f1oeq3  6761  foeq123d  6764  resdif  6792  ncanth  7315  ffoss  7892  rneqdmfinf1o  9237  fidomdm  9238  fifo  9339  brwdom  9476  brwdom2  9482  canthwdom  9488  ixpiunwdom  9499  fin1a2lem7  10323  dmct  10441  s7f1o  14923  znnen  16174  quslem  17502  znzrhfo  21526  rncmp  23383  connima  23412  conncn  23413  qtopcmplem  23694  qtoprest  23704  eupths  30292  pjhfo  31799  2ndresdjuf1o  32746  cycpmconjvlem  33226  algextdeglem8  33920  msrfo  35789  ivthALT  36578  bj-inftyexpitaufo  37577  poimirlem26  38028  poimirlem27  38029  opidon2OLD  38236  founiiun0  45651  focofob  47557  fundcmpsurinj  47898  fundcmpsurbijinj  47899  imasubc  49655  fullthinc  49954