|   | 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 6585 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺)) | |
| 2 | dmeq 5913 | . . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺) | |
| 3 | 2 | eqeq1d 2738 | . . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴)) | 
| 4 | 1, 3 | anbi12d 632 | . 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))) | 
| 5 | df-fn 6563 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 6 | df-fn 6563 | . 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 1539 dom cdm 5684 Fun wfun 6554 Fn wfn 6555 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 df-opab 5205 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-fun 6562 df-fn 6563 | 
| This theorem is referenced by: fneq1d 6660 fneq1i 6664 fn0 6698 feq1 6715 foeq1 6815 f1ocnv 6859 dffn5 6966 mpteqb 7034 fnsnbg 7185 fnsnbOLD 7187 fnprb 7229 fntpb 7230 eufnfv 7250 frrlem1 8312 frrlem13 8324 wfrlem1OLD 8349 wfrlem3OLDa 8352 wfrlem15OLD 8364 tfrlem12 8430 fsetdmprc0 8896 mapval2 8913 elixp2 8942 ixpfn 8944 elixpsn 8978 inf3lem6 9674 ssttrcl 9756 ttrcltr 9757 ttrclss 9761 ttrclselem2 9767 aceq3lem 10161 dfac4 10163 dfacacn 10183 axcc2lem 10477 axcc3 10479 seqof 14101 ccatvalfn 14620 cshword 14830 0csh0 14832 rrgsupp 20702 lmodfopnelem1 20897 elpt 23581 elptr 23582 ptcmplem3 24063 prdsxmslem2 24543 tgjustr 28483 bnj62 34735 bnj976 34792 bnj66 34875 bnj124 34886 bnj607 34931 bnj873 34939 bnj1234 35028 bnj1463 35070 fineqvac 35112 gblacfnacd 35114 eqresfnbd 42273 dssmapf1od 44039 fnchoice 45039 choicefi 45210 axccdom 45232 dfafn5b 47178 rngchomffvalALTV 48199 functhinclem1 49118 | 
| Copyright terms: Public domain | W3C validator |