Theorem foeq3 6791

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ran crn 5663   Fn wfn 6532  –onto→wfo 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fo 6543

This theorem is referenced by:  fimadmfo  6802  f1oeq3  6811  foeq123d  6814  resdif  6843  ncanth  7366  ffoss  7943  rneqdmfinf1o  9290  fidomdm  9291  fifo  9392  brwdom  9529  brwdom2  9535  canthwdom  9541  ixpiunwdom  9552  fin1a2lem7  10390  dmct  10508  s7f1o  15003  znnen  16268  quslem  17597  znzrhfo  21666  rncmp  23522  connima  23551  conncn  23552  qtopcmplem  23833  qtoprest  23843  eupths  30492  pjhfo  31999  2ndresdjuf1o  32936  cycpmconjvlem  33402  algextdeglem8  34059  msrfo  35971  ivthALT  36769  bj-inftyexpitaufo  37769  poimirlem26  38220  poimirlem27  38221  opidon2OLD  38428  founiiun0  45835  focofob  47741  fundcmpsurinj  48082  fundcmpsurbijinj  48083  imasubc  49849  fullthinc  50148