|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > foeq3 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) | 
| Ref | Expression | 
|---|---|
| foeq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqeq2 2748 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
| 2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) | 
| 3 | df-fo 6566 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
| 4 | df-fo 6566 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ran crn 5685 Fn wfn 6555 –onto→wfo 6558 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-fo 6566 | 
| This theorem is referenced by: fimadmfo 6828 f1oeq3 6837 foeq123d 6840 resdif 6868 ncanth 7387 ffoss 7971 rneqdmfinf1o 9374 fidomdm 9375 fifo 9473 brwdom 9608 brwdom2 9614 canthwdom 9620 ixpiunwdom 9631 fin1a2lem7 10447 dmct 10565 s7f1o 15006 znnen 16249 quslem 17589 znzrhfo 21567 rncmp 23405 connima 23434 conncn 23435 qtopcmplem 23716 qtoprest 23726 eupths 30220 pjhfo 31726 2ndresdjuf1o 32661 cycpmconjvlem 33162 algextdeglem8 33766 msrfo 35552 ivthALT 36337 bj-inftyexpitaufo 37204 poimirlem26 37654 poimirlem27 37655 opidon2OLD 37862 founiiun0 45200 focofob 47097 fundcmpsurinj 47401 fundcmpsurbijinj 47402 fullthinc 49124 | 
| Copyright terms: Public domain | W3C validator |