Theorem foeq3 6794

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 6544	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6544	. 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 1569  ran crn 5651   Fn wfn 6533  –onto→wfo 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  fimadmfo  6805  f1oeq3  6814  foeq123d  6817  resdif  6846  ncanth  7375  ffoss  7958  rneqdmfinf1o  9322  fidomdm  9323  fifo  9424  brwdom  9561  brwdom2  9567  canthwdom  9573  ixpiunwdom  9584  fin1a2lem7  10484  dmct  10602  dmctOLD  10603  s7f1o  15119  znnen  16380  quslem  17715  znzrhfo  21853  rncmp  23714  connima  23743  conncn  23744  qtopcmplem  24026  qtoprest  24036  eupths  30801  pjhfo  32308  2ndresdjuf1o  33244  cycpmconjvlem  33702  algextdeglem8  34356  msrfo  36311  ivthALT  37123  bj-inftyexpitaufo  38124  poimirlem26  38565  poimirlem27  38566  opidon2OLD  38789  founiiun0  46205  focofob  48150  fundcmpsurinj  48491  fundcmpsurbijinj  48492  imasubc  50259  fullthinc  50558