Theorem foeq3 6745

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 6499	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6499	. 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 5626   Fn wfn 6488  –onto→wfo 6491

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 6499

This theorem is referenced by:  fimadmfo  6756  f1oeq3  6765  foeq123d  6768  resdif  6796  ncanth  7315  ffoss  7892  rneqdmfinf1o  9237  fidomdm  9238  fifo  9339  brwdom  9476  brwdom2  9482  canthwdom  9488  ixpiunwdom  9499  fin1a2lem7  10320  dmct  10438  s7f1o  14893  znnen  16141  quslem  17468  znzrhfo  21506  rncmp  23344  connima  23373  conncn  23374  qtopcmplem  23655  qtoprest  23665  eupths  30279  pjhfo  31785  2ndresdjuf1o  32731  cycpmconjvlem  33225  algextdeglem8  33883  msrfo  35742  ivthALT  36531  bj-inftyexpitaufo  37409  poimirlem26  37849  poimirlem27  37850  opidon2OLD  38057  founiiun0  45501  focofob  47393  fundcmpsurinj  47722  fundcmpsurbijinj  47723  imasubc  49463  fullthinc  49762