|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > fneq2i | Structured version Visualization version GIF version | ||
| Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.) | 
| Ref | Expression | 
|---|---|
| fneq2i.1 | ⊢ 𝐴 = 𝐵 | 
| Ref | Expression | 
|---|---|
| fneq2i | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | fneq2i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | fneq2 6659 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 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-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-fn 6563 | 
| This theorem is referenced by: fnunop 6683 fnprb 7229 fntpb 7230 fnsuppeq0 8218 tpos0 8282 wfrlem5OLD 8354 dfixp 8940 ordtypelem4 9562 ser0f 14097 0csh0 14832 s3fn 14951 prodf1f 15929 efcvgfsum 16123 prmrec 16961 fnpr2o 17603 0ssc 17883 0subcat 17884 mulgfvi 19092 ovolunlem1 25533 volsup 25592 mtest 26448 mtestbdd 26449 pserulm 26466 pserdvlem2 26473 emcllem5 27044 lgamgulm2 27080 lgamcvglem 27084 gamcvg2lem 27103 tglnfn 28556 crctcshlem4 29841 fsuppcurry1 32737 fsuppcurry2 32738 resf1o 32742 s2rnOLD 32929 s3rnOLD 32931 cycpmfvlem 33133 cycpmfv3 33136 esumfsup 34072 esumpcvgval 34080 esumcvg 34088 esumsup 34091 bnj149 34890 bnj1312 35073 faclimlem1 35744 fullfunfnv 35948 ixpeq1i 36202 cbvixpvw2 36247 knoppcnlem8 36502 knoppcnlem11 36505 mblfinlem2 37666 ovoliunnfl 37670 voliunnfl 37672 subsaliuncl 46378 fcores 47084 isubgr3stgrlem7 47944 0funcALT 48937 | 
| Copyright terms: Public domain | W3C validator |