| 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 6506 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺)) | |
| 2 | dmeq 5850 | . . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺) | |
| 3 | 2 | eqeq1d 2731 | . . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴)) |
| 4 | 1, 3 | anbi12d 632 | . 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))) |
| 5 | df-fn 6489 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 6 | df-fn 6489 | . 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)) | |
| 7 | 4, 5, 6 | 3bitr4g 314 | 1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 dom cdm 5623 Fun wfun 6480 Fn wfn 6481 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3397 df-v 3440 df-dif 3908 df-un 3910 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-br 5096 df-opab 5158 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-fun 6488 df-fn 6489 |
| This theorem is referenced by: fneq1d 6579 fneq1i 6583 fn0 6617 feq1 6634 foeq1 6736 f1ocnv 6780 dffn5 6885 mpteqb 6953 fnsnbg 7104 fnsnbOLD 7106 fnprb 7148 fntpb 7149 eufnfv 7169 frrlem1 8226 frrlem13 8238 tfrlem12 8318 fsetdmprc0 8789 mapval2 8806 elixp2 8835 ixpfn 8837 elixpsn 8871 inf3lem6 9548 ssttrcl 9630 ttrcltr 9631 ttrclss 9635 ttrclselem2 9641 aceq3lem 10033 dfac4 10035 dfacacn 10055 axcc2lem 10349 axcc3 10351 seqof 13985 ccatvalfn 14507 cshword 14716 0csh0 14718 rrgsupp 20605 lmodfopnelem1 20820 elpt 23476 elptr 23477 ptcmplem3 23958 prdsxmslem2 24434 tgjustr 28438 bnj62 34706 bnj976 34763 bnj66 34846 bnj124 34857 bnj607 34902 bnj873 34910 bnj1234 34999 bnj1463 35041 fineqvac 35091 gblacfnacd 35094 eqresfnbd 42225 dssmapf1od 44014 fnchoice 45027 choicefi 45198 axccdom 45220 dfafn5b 47165 rngchomffvalALTV 48282 ixpv 48894 iinfconstbaslem 49070 iinfconstbas 49071 nelsubc3lem 49075 functhinclem1 49449 cnelsubclem 49608 |
| Copyright terms: Public domain | W3C validator |