Theorem foeq3 6791

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5660   Fn wfn 6532  –onto→wfo 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-fo 6543

This theorem is used by:  fimadmfo  6802  f1oeq3  6811  foeq123d  6814  resdif  6843  ncanth  7371  ffoss  7946  rneqdmfinf1o  9303  fidomdm  9304  fifo  9405  brwdom  9542  brwdom2  9548  canthwdom  9554  ixpiunwdom  9565  fin1a2lem7  10411  dmct  10529  dmctOLD  10530  s7f1o  15041  znnen  16304  quslem  17633  znzrhfo  21761  rncmp  23622  connima  23651  conncn  23652  qtopcmplem  23934  qtoprest  23944  eupths  30666  pjhfo  32173  2ndresdjuf1o  33110  cycpmconjvlem  33568  algextdeglem8  34221  msrfo  36112  ivthALT  36941  bj-inftyexpitaufo  37941  poimirlem26  38382  poimirlem27  38383  opidon2OLD  38591  founiiun0  46009  focofob  47955  fundcmpsurinj  48296  fundcmpsurbijinj  48297  imasubc  50064  fullthinc  50363