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 6439 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 Fn wfn 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-fn 6352 |
This theorem is referenced by: fnunsn 6458 fnprb 6963 fntpb 6964 fnsuppeq0 7849 tpos0 7913 wfrlem5 7950 dfixp 8452 ordtypelem4 8974 ser0f 13413 0csh0 14145 s3fn 14263 prodf1f 15238 efcvgfsum 15429 prmrec 16248 fnpr2o 16820 0ssc 17097 0subcat 17098 mulgfvi 18170 ovolunlem1 24027 volsup 24086 mtest 24921 mtestbdd 24922 pserulm 24939 pserdvlem2 24945 emcllem5 25505 lgamgulm2 25541 lgamcvglem 25545 gamcvg2lem 25564 tglnfn 26261 crctcshlem4 27526 fsuppcurry1 30388 fsuppcurry2 30389 resf1o 30393 s2rn 30548 s3rn 30550 cycpmfvlem 30682 cycpmfv3 30685 esumfsup 31229 esumpcvgval 31237 esumcvg 31245 esumsup 31248 bnj149 32047 bnj1312 32228 faclimlem1 32873 fullfunfnv 33305 knoppcnlem8 33737 knoppcnlem11 33740 mblfinlem2 34812 ovoliunnfl 34816 voliunnfl 34818 subsaliuncl 42522 |
Copyright terms: Public domain | W3C validator |