Theorem foeq3 6746

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5627   Fn wfn 6489  –onto→wfo 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fo 6500

This theorem is referenced by:  fimadmfo  6757  f1oeq3  6766  foeq123d  6769  resdif  6797  ncanth  7317  ffoss  7894  rneqdmfinf1o  9238  fidomdm  9239  fifo  9340  brwdom  9477  brwdom2  9483  canthwdom  9489  ixpiunwdom  9500  fin1a2lem7  10323  dmct  10441  s7f1o  14923  znnen  16174  quslem  17502  znzrhfo  21541  rncmp  23375  connima  23404  conncn  23405  qtopcmplem  23686  qtoprest  23696  eupths  30289  pjhfo  31796  2ndresdjuf1o  32742  cycpmconjvlem  33221  algextdeglem8  33888  msrfo  35748  ivthALT  36537  bj-inftyexpitaufo  37536  poimirlem26  37987  poimirlem27  37988  opidon2OLD  38195  founiiun0  45644  focofob  47546  fundcmpsurinj  47887  fundcmpsurbijinj  47888  imasubc  49644  fullthinc  49943