Theorem foeq3 6351

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656  ran crn 5343   Fn wfn 6118  –onto→wfo 6121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-fo 6129

This theorem is referenced by:  fimadmfo  6362  f1oeq3  6369  foeq123d  6372  resdif  6398  ffoss  7389  rneqdmfinf1o  8511  fidomdm  8512  fifo  8607  brwdom  8741  brwdom2  8747  canthwdom  8753  ixpiunwdom  8765  fin1a2lem7  9543  dmct  9661  znnen  15315  quslem  16556  znzrhfo  20255  rncmp  21570  connima  21599  conncn  21600  qtopcmplem  21881  qtoprest  21891  eupths  27565  pjhfo  29109  msrfo  31978  ivthALT  32857  bj-inftyexpitaufo  33621  poimirlem26  33972  poimirlem27  33973  opidon2OLD  34188  founiiun0  40178