![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > foeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
foeq1 | ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 6591 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
2 | rneq 5890 | . . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺) | |
3 | 2 | eqeq1d 2738 | . . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 = 𝐵 ↔ ran 𝐺 = 𝐵)) |
4 | 1, 3 | anbi12d 631 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵))) |
5 | df-fo 6500 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
6 | df-fo 6500 | . 2 ⊢ (𝐺:𝐴–onto→𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 = 𝐵)) | |
7 | 4, 5, 6 | 3bitr4g 313 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ran crn 5633 Fn wfn 6489 –onto→wfo 6492 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-fun 6496 df-fn 6497 df-fo 6500 |
This theorem is referenced by: fimadmfoALT 6765 f1oeq1 6770 foeq123d 6775 resdif 6803 exfo 7052 mapfoss 8787 fodomr 9069 dif1enlem 9097 dif1enlemOLD 9098 fowdom 9504 brwdom2 9506 canthp1lem2 10586 mndfo 18577 sursubmefmnd 18703 znzrhfo 20950 pjhfo 30546 elunop 30712 elunop2 30853 symgcom 31829 nnfoctbdjlem 44666 fcoreslem3 45269 fcoresfo 45275 fcoresfob 45276 fundcmpsurbijinjpreimafv 45569 |
Copyright terms: Public domain | W3C validator |