![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfeq | Structured version Visualization version GIF version |
Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
Ref | Expression |
---|---|
nfnfc.1 | ⊢ Ⅎ𝑥𝐴 |
nfeq.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfeq | ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnfc.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
3 | nfeq.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐵) |
5 | 2, 4 | nfeqd 2917 | . 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵) |
6 | 5 | mptru 1548 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ⊤wtru 1542 Ⅎwnf 1785 Ⅎwnfc 2887 |
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-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-cleq 2728 df-nfc 2889 |
This theorem is referenced by: nfeq1 2922 nfeq2 2924 nfne 3045 raleqf 3328 rexeqf 3329 rmoeq1f 3395 reueq1f 3396 rabeqf 3438 csbhypf 3884 sbceqg 4369 nffn 6601 nffo 6755 fvmptd3f 6963 mpteqb 6967 fvmptf 6969 eqfnfv2f 6986 dff13f 7202 ovmpos 7502 ov2gf 7503 ovmpodxf 7504 ovmpodf 7510 eqerlem 8681 seqof2 13965 sumeq2ii 15577 sumss 15608 fsumadd 15624 fsummulc2 15668 fsumrelem 15691 prodeq1f 15790 prodeq2ii 15795 fprodmul 15842 fproddiv 15843 txcnp 22969 ptcnplem 22970 cnmpt11 23012 cnmpt21 23020 cnmptcom 23027 mbfeqalem1 25003 mbflim 25030 itgeq1f 25134 itgeqa 25176 dvmptfsum 25337 ulmss 25754 leibpi 26290 o1cxp 26322 lgseisenlem2 26722 nosupbnd1 27060 2ndresdju 31512 aciunf1lem 31525 sigapildsys 32701 bnj1316 33372 bnj1446 33597 bnj1447 33598 bnj1448 33599 bnj1519 33617 bnj1520 33618 bnj1529 33622 subtr 34776 subtr2 34777 bj-sbeqALT 35357 poimirlem25 36093 iuneq2f 36605 mpobi123f 36611 mptbi12f 36615 dvdsrabdioph 41110 fphpd 41116 mnringmulrcld 42489 fvelrnbf 43204 refsum2cnlem1 43223 elrnmpt1sf 43383 choicefi 43396 axccdom 43418 uzublem 43640 fsumf1of 43786 fmuldfeq 43795 mccl 43810 climmulf 43816 climexp 43817 climsuse 43820 climrecf 43821 climaddf 43827 mullimc 43828 neglimc 43859 addlimc 43860 0ellimcdiv 43861 climeldmeqmpt 43880 climfveqmpt 43883 climfveqf 43892 climfveqmpt3 43894 climeldmeqf 43895 climeqf 43900 climeldmeqmpt3 43901 limsupubuzlem 43924 limsupequz 43935 dvnmptdivc 44150 dvmptfprod 44157 dvnprodlem1 44158 stoweidlem18 44230 stoweidlem31 44243 stoweidlem55 44267 stoweidlem59 44271 sge0f1o 44594 sge0iunmpt 44630 sge0reuz 44659 iundjiun 44672 hoicvrrex 44768 ovnhoilem1 44813 ovnlecvr2 44822 opnvonmbllem1 44844 vonioo 44894 vonicc 44897 sssmf 44950 smflim 44989 smfpimcclem 45019 smfpimcc 45020 cfsetsnfsetf 45263 ovmpordxf 46385 |
Copyright terms: Public domain | W3C validator |