| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fneq2d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
| Ref | Expression |
|---|---|
| fneq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| fneq2d | ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fneq2d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | fneq2 6660 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 Fn wfn 6556 |
| 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 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fn 6564 |
| This theorem is referenced by: fneq12d 6663 fncofn 6685 fnco 6686 fnprb 7228 fntpb 7229 fnpr2g 7230 undifixp 8974 brwdom2 9613 brttrcl2 9754 ssttrcl 9755 ttrcltr 9756 ttrclss 9760 ttrclselem2 9766 dfac3 10161 ac7g 10514 ccatlid 14624 ccatrid 14625 ccatass 14626 ccatswrd 14706 swrdccat2 14707 ccatpfx 14739 swrdswrd 14743 swrdccatin2 14767 pfxccatin12 14771 revccat 14804 revrev 14805 repsdf2 14816 0csh0 14831 cshco 14875 wrd2pr2op 14982 wrd3tpop 14987 ofccat 15008 seqshft 15124 invf 17812 sscfn1 17861 sscfn2 17862 isssc 17864 fuchom 18009 estrchomfeqhom 18180 mulgfval 19087 mulgfvalALT 19088 srhmsubc 20680 frlmsslss2 21795 subrgascl 22090 m1detdiag 22603 ptval 23578 xpsdsfn2 24388 fresf1o 32641 psgndmfi 33118 cycpmconjslem1 33174 cycpmconjslem2 33175 ply1annidllem 33744 pl1cn 33954 signsvtn0 34585 signstres 34590 bnj927 34783 fineqvac 35111 revpfxsfxrev 35121 ixpeq12dv 36217 cbvixpdavw 36279 cbvixpdavw2 36295 poimirlem1 37628 poimirlem2 37629 poimirlem3 37630 poimirlem4 37631 poimirlem6 37633 poimirlem7 37634 poimirlem11 37638 poimirlem12 37639 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 dibfnN 41158 dihintcl 41346 frlmvscadiccat 42516 selvvvval 42595 ofoafg 43367 uzmptshftfval 44365 srhmsubcALTV 48241 tposideq 48788 0funcg2 48917 fucofulem2 49006 |
| Copyright terms: Public domain | W3C validator |