Theorem foeq3 6588

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ran crn 5556   Fn wfn 6350  –onto→wfo 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-fo 6361

This theorem is referenced by:  fimadmfo  6599  f1oeq3  6606  foeq123d  6609  resdif  6635  ncanth  7112  ffoss  7647  rneqdmfinf1o  8800  fidomdm  8801  fifo  8896  brwdom  9031  brwdom2  9037  canthwdom  9043  ixpiunwdom  9055  fin1a2lem7  9828  dmct  9946  znnen  15565  quslem  16816  znzrhfo  20694  rncmp  22004  connima  22033  conncn  22034  qtopcmplem  22315  qtoprest  22325  eupths  27979  pjhfo  29483  cycpmconjvlem  30783  msrfo  32793  ivthALT  33683  bj-inftyexpitaufo  34487  poimirlem26  34933  poimirlem27  34934  opidon2OLD  35147  founiiun0  41471  fundcmpsurinj  43589  fundcmpsurbijinj  43590