Theorem foeq3 6151

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ran crn 5144   Fn wfn 5921  –onto→wfo 5924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fo 5932

This theorem is referenced by:  f1oeq3  6167  foeq123d  6170  resdif  6195  ffoss  7169  rneqdmfinf1o  8283  fidomdm  8284  fifo  8379  brwdom  8513  brwdom2  8519  canthwdom  8525  ixpiunwdom  8537  fin1a2lem7  9266  dmct  9384  znnen  14985  quslem  16250  znzrhfo  19944  rncmp  21247  connima  21276  conncn  21277  qtopcmplem  21558  qtoprest  21568  eupths  27178  pjhfo  28693  msrfo  31569  ivthALT  32455  poimirlem26  33565  poimirlem27  33566  opidon2OLD  33783  founiiun0  39691