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 2745	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 630	. 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 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

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

This theorem is referenced by:  fimadmfo  6752  f1oeq3  6761  foeq123d  6764  resdif  6792  ncanth  7310  ffoss  7887  rneqdmfinf1o  9227  fidomdm  9228  fifo  9326  brwdom  9463  brwdom2  9469  canthwdom  9475  ixpiunwdom  9486  fin1a2lem7  10307  dmct  10425  s7f1o  14883  znnen  16131  quslem  17457  znzrhfo  21494  rncmp  23321  connima  23350  conncn  23351  qtopcmplem  23632  qtoprest  23642  eupths  30191  pjhfo  31697  2ndresdjuf1o  32643  cycpmconjvlem  33121  algextdeglem8  33748  msrfo  35601  ivthALT  36390  bj-inftyexpitaufo  37257  poimirlem26  37696  poimirlem27  37697  opidon2OLD  37904  founiiun0  45301  focofob  47194  fundcmpsurinj  47523  fundcmpsurbijinj  47524  imasubc  49266  fullthinc  49565