![]() |
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 6638 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 Fn wfn 6535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2724 df-fn 6543 |
This theorem is referenced by: fnunop 6662 fnprb 7206 fntpb 7207 fnsuppeq0 8173 tpos0 8237 wfrlem5OLD 8309 dfixp 8889 ordtypelem4 9512 ser0f 14017 0csh0 14739 s3fn 14858 prodf1f 15834 efcvgfsum 16025 prmrec 16851 fnpr2o 17499 0ssc 17783 0subcat 17784 mulgfvi 18950 ovolunlem1 25005 volsup 25064 mtest 25907 mtestbdd 25908 pserulm 25925 pserdvlem2 25931 emcllem5 26493 lgamgulm2 26529 lgamcvglem 26533 gamcvg2lem 26552 tglnfn 27787 crctcshlem4 29063 fsuppcurry1 31937 fsuppcurry2 31938 resf1o 31942 s2rn 32097 s3rn 32099 cycpmfvlem 32258 cycpmfv3 32261 esumfsup 33056 esumpcvgval 33064 esumcvg 33072 esumsup 33075 bnj149 33874 bnj1312 34057 faclimlem1 34701 fullfunfnv 34906 knoppcnlem8 35364 knoppcnlem11 35367 mblfinlem2 36514 ovoliunnfl 36518 voliunnfl 36520 subsaliuncl 45060 fcores 45763 |
Copyright terms: Public domain | W3C validator |