Theorem foeq3 6773

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5642   Fn wfn 6509  –onto→wfo 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fo 6520

This theorem is referenced by:  fimadmfo  6784  f1oeq3  6793  foeq123d  6796  resdif  6824  ncanth  7345  ffoss  7927  rneqdmfinf1o  9291  fidomdm  9292  fifo  9390  brwdom  9527  brwdom2  9533  canthwdom  9539  ixpiunwdom  9550  fin1a2lem7  10366  dmct  10484  s7f1o  14939  znnen  16187  quslem  17513  znzrhfo  21464  rncmp  23290  connima  23319  conncn  23320  qtopcmplem  23601  qtoprest  23611  eupths  30136  pjhfo  31642  2ndresdjuf1o  32581  cycpmconjvlem  33105  algextdeglem8  33721  msrfo  35540  ivthALT  36330  bj-inftyexpitaufo  37197  poimirlem26  37647  poimirlem27  37648  opidon2OLD  37855  founiiun0  45191  focofob  47085  fundcmpsurinj  47414  fundcmpsurbijinj  47415  imasubc  49144  fullthinc  49443