Theorem foeq3 6783

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5649   Fn wfn 6523  –onto→wfo 6526

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fo 6534

This theorem is used by:  fimadmfo  6794  f1oeq3  6803  foeq123d  6806  resdif  6835  ncanth  7364  ffoss  7942  rneqdmfinf1o  9300  fidomdm  9301  fifo  9402  brwdom  9539  brwdom2  9545  canthwdom  9551  ixpiunwdom  9562  fin1a2lem7  10441  dmct  10559  dmctOLD  10560  s7f1o  15072  znnen  16333  quslem  17662  znzrhfo  21800  rncmp  23661  connima  23690  conncn  23691  qtopcmplem  23973  qtoprest  23983  eupths  30720  pjhfo  32227  2ndresdjuf1o  33163  cycpmconjvlem  33621  algextdeglem8  34275  msrfo  36226  ivthALT  37039  bj-inftyexpitaufo  38037  poimirlem26  38478  poimirlem27  38479  opidon2OLD  38702  founiiun0  46120  focofob  48066  fundcmpsurinj  48407  fundcmpsurbijinj  48408  imasubc  50175  fullthinc  50474