Theorem foeq3 6832

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ran crn 5701   Fn wfn 6568  –onto→wfo 6571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fo 6579

This theorem is referenced by:  fimadmfo  6843  f1oeq3  6852  foeq123d  6855  resdif  6883  ncanth  7402  ffoss  7986  rneqdmfinf1o  9401  fidomdm  9402  fifo  9501  brwdom  9636  brwdom2  9642  canthwdom  9648  ixpiunwdom  9659  fin1a2lem7  10475  dmct  10593  s7f1o  15015  znnen  16260  quslem  17603  znzrhfo  21589  rncmp  23425  connima  23454  conncn  23455  qtopcmplem  23736  qtoprest  23746  eupths  30232  pjhfo  31738  2ndresdjuf1o  32668  cycpmconjvlem  33134  algextdeglem8  33715  msrfo  35514  ivthALT  36301  bj-inftyexpitaufo  37168  poimirlem26  37606  poimirlem27  37607  opidon2OLD  37814  founiiun0  45097  focofob  46995  fundcmpsurinj  47283  fundcmpsurbijinj  47284  fullthinc  48713