![]() |
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 6568 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺)) | |
2 | dmeq 5903 | . . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺) | |
3 | 2 | eqeq1d 2733 | . . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴)) |
4 | 1, 3 | anbi12d 630 | . 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))) |
5 | df-fn 6546 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
6 | df-fn 6546 | . 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)) | |
7 | 4, 5, 6 | 3bitr4g 314 | 1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1540 dom cdm 5676 Fun wfun 6537 Fn wfn 6538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-fun 6545 df-fn 6546 |
This theorem is referenced by: fneq1d 6642 fneq1i 6646 fn0 6681 feq1 6698 foeq1 6801 f1ocnv 6845 dffn5 6950 mpteqb 7017 fnsnb 7166 fnprb 7212 fntpb 7213 eufnfv 7233 frrlem1 8277 frrlem13 8289 wfrlem1OLD 8314 wfrlem3OLDa 8317 wfrlem15OLD 8329 tfrlem12 8395 fsetdmprc0 8855 mapval2 8872 elixp2 8901 ixpfn 8903 elixpsn 8937 inf3lem6 9634 ssttrcl 9716 ttrcltr 9717 ttrclss 9721 ttrclselem2 9727 aceq3lem 10121 dfac4 10123 dfacacn 10142 axcc2lem 10437 axcc3 10439 seqof 14032 ccatvalfn 14538 cshword 14748 0csh0 14750 lmodfopnelem1 20740 rrgsupp 21196 elpt 23396 elptr 23397 ptcmplem3 23878 prdsxmslem2 24358 tgjustr 28158 bnj62 34195 bnj976 34252 bnj66 34335 bnj124 34346 bnj607 34391 bnj873 34399 bnj1234 34488 bnj1463 34530 fineqvac 34561 fnsnbt 41518 eqresfnbd 41521 dssmapf1od 43235 fnchoice 44176 choicefi 44358 axccdom 44380 dfafn5b 46328 rngchomffvalALTV 47115 functhinclem1 47823 |
Copyright terms: Public domain | W3C validator |