![]() |
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 6067 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺)) | |
2 | dmeq 5477 | . . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺) | |
3 | 2 | eqeq1d 2760 | . . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴)) |
4 | 1, 3 | anbi12d 749 | . 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))) |
5 | df-fn 6050 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
6 | df-fn 6050 | . 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)) | |
7 | 4, 5, 6 | 3bitr4g 303 | 1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1630 dom cdm 5264 Fun wfun 6041 Fn wfn 6042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-rab 3057 df-v 3340 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-sn 4320 df-pr 4322 df-op 4326 df-br 4803 df-opab 4863 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-fun 6049 df-fn 6050 |
This theorem is referenced by: fneq1d 6140 fneq1i 6144 fn0 6170 feq1 6185 foeq1 6270 f1ocnv 6308 dffn5 6401 mpteqb 6459 fnsnb 6594 fnprb 6634 fntpb 6635 eufnfv 6652 wfrlem1 7581 wfrlem3a 7584 wfrlem15 7596 tfrlem12 7652 mapval2 8051 elixp2 8076 ixpfn 8078 elixpsn 8111 inf3lem6 8701 aceq3lem 9131 dfac4 9133 dfacacn 9153 axcc2lem 9448 axcc3 9450 seqof 13050 ccatvalfn 13551 cshword 13735 0csh0 13737 lmodfopnelem1 19099 rrgsupp 19491 elpt 21575 elptr 21576 ptcmplem3 22057 prdsxmslem2 22533 bnj62 31093 bnj976 31153 bnj66 31235 bnj124 31246 bnj607 31291 bnj873 31299 bnj1234 31386 bnj1463 31428 frrlem1 32084 dssmapf1od 38815 fnchoice 39685 choicefi 39889 axccdom 39913 dfafn5b 41745 cshword2 41945 rngchomffvalALTV 42503 |
Copyright terms: Public domain | W3C validator |