| 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 2916 | . 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵) |
| 6 | 5 | mptru 1547 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ⊤wtru 1541 Ⅎwnf 1783 Ⅎwnfc 2890 |
| 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-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-nfc 2892 |
| This theorem is referenced by: nfeq1 2921 nfeq2 2923 nfne 3043 raleqf 3353 rexeqfOLD 3355 rmoeq1f 3424 rabeqf 3472 csbhypf 3927 sbceqg 4412 nffn 6667 nffo 6819 fvmptd3f 7031 mpteqb 7035 fvmptf 7037 eqfnfv2f 7055 dff13f 7276 ovmpos 7581 ov2gf 7582 ovmpodxf 7583 ovmpodf 7589 eqerlem 8780 seqof2 14101 sumeq2ii 15729 sumss 15760 fsumadd 15776 fsummulc2 15820 fsumrelem 15843 prodeq1f 15942 prodeq2ii 15947 fprodmul 15996 fproddiv 15997 txcnp 23628 ptcnplem 23629 cnmpt11 23671 cnmpt21 23679 cnmptcom 23686 mbfeqalem1 25676 mbflim 25703 itgeq1f 25806 itgeq1fOLD 25807 itgeqa 25849 dvmptfsum 26013 ulmss 26440 leibpi 26985 o1cxp 27018 lgseisenlem2 27420 nosupbnd1 27759 2ndresdju 32659 aciunf1lem 32672 sigapildsys 34163 bnj1316 34834 bnj1446 35059 bnj1447 35060 bnj1448 35061 bnj1519 35079 bnj1520 35080 bnj1529 35084 subtr 36315 subtr2 36316 bj-sbeqALT 36901 poimirlem25 37652 iuneq2f 38163 mpobi123f 38169 mptbi12f 38173 dvdsrabdioph 42821 fphpd 42827 mnringmulrcld 44247 fvelrnbf 45023 refsum2cnlem1 45042 elrnmpt1sf 45194 choicefi 45205 axccdom 45227 uzublem 45441 fsumf1of 45589 fmuldfeq 45598 mccl 45613 climmulf 45619 climexp 45620 climsuse 45623 climrecf 45624 climaddf 45630 mullimc 45631 neglimc 45662 addlimc 45663 0ellimcdiv 45664 climeldmeqmpt 45683 climfveqmpt 45686 climfveqf 45695 climfveqmpt3 45697 climeldmeqf 45698 climeqf 45703 climeldmeqmpt3 45704 limsupubuzlem 45727 limsupequz 45738 dvnmptdivc 45953 dvmptfprod 45960 stoweidlem18 46033 stoweidlem31 46046 stoweidlem55 46070 stoweidlem59 46074 sge0iunmpt 46433 sge0reuz 46462 iundjiun 46475 hoicvrrex 46571 ovnhoilem1 46616 ovnlecvr2 46625 opnvonmbllem1 46647 vonioo 46697 vonicc 46700 sssmf 46753 smflim 46792 smfpimcclem 46822 smfpimcc 46823 cfsetsnfsetf 47070 ovmpordxf 48255 |
| Copyright terms: Public domain | W3C validator |