Theorem foeq3 6770

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 2741	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵))
2	1	anbi2d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)))
3		df-fo 6517	. 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴))
4		df-fo 6517	. 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 5639   Fn wfn 6506  –onto→wfo 6509

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 2701

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

This theorem is referenced by:  fimadmfo  6781  f1oeq3  6790  foeq123d  6793  resdif  6821  ncanth  7342  ffoss  7924  rneqdmfinf1o  9284  fidomdm  9285  fifo  9383  brwdom  9520  brwdom2  9526  canthwdom  9532  ixpiunwdom  9543  fin1a2lem7  10359  dmct  10477  s7f1o  14932  znnen  16180  quslem  17506  znzrhfo  21457  rncmp  23283  connima  23312  conncn  23313  qtopcmplem  23594  qtoprest  23604  eupths  30129  pjhfo  31635  2ndresdjuf1o  32574  cycpmconjvlem  33098  algextdeglem8  33714  msrfo  35533  ivthALT  36323  bj-inftyexpitaufo  37190  poimirlem26  37640  poimirlem27  37641  opidon2OLD  37848  founiiun0  45184  focofob  47081  fundcmpsurinj  47410  fundcmpsurbijinj  47411  imasubc  49140  fullthinc  49439