![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fneq1 | Structured version Visualization version GIF version |
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fneq1 | ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funeq 6208 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺)) | |
2 | dmeq 5622 | . . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺) | |
3 | 2 | eqeq1d 2780 | . . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴)) |
4 | 1, 3 | anbi12d 621 | . 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))) |
5 | df-fn 6191 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
6 | df-fn 6191 | . 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)) | |
7 | 4, 5, 6 | 3bitr4g 306 | 1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 dom cdm 5407 Fun wfun 6182 Fn wfn 6183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-fun 6190 df-fn 6191 |
This theorem is referenced by: fneq1d 6279 fneq1i 6283 fn0 6309 feq1 6325 foeq1 6415 f1ocnv 6456 dffn5 6554 mpteqb 6613 fnsnb 6751 fnprb 6797 fntpb 6798 eufnfv 6817 wfrlem1 7757 wfrlem3a 7760 wfrlem15 7773 tfrlem12 7829 mapval2 8236 elixp2 8263 ixpfn 8265 elixpsn 8298 inf3lem6 8890 aceq3lem 9340 dfac4 9342 dfacacn 9361 axcc2lem 9656 axcc3 9658 seqof 13242 ccatvalfn 13744 cshword 14013 0csh0 14016 0csh0OLD 14017 lmodfopnelem1 19392 rrgsupp 19785 elpt 21884 elptr 21885 ptcmplem3 22366 prdsxmslem2 22842 tgjustr 25962 bnj62 31644 bnj976 31703 bnj66 31785 bnj124 31796 bnj607 31841 bnj873 31849 bnj1234 31936 bnj1463 31978 frrlem1 32650 frrlem13 32662 fnsnbt 38571 dssmapf1od 39736 fnchoice 40711 choicefi 40894 axccdom 40918 dfafn5b 42772 rngchomffvalALTV 43636 |
Copyright terms: Public domain | W3C validator |