![]() |
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 2902 | . 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵) |
6 | 5 | trud 1634 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1624 ⊤wtru 1625 Ⅎwnf 1849 Ⅎwnfc 2881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-cleq 2745 df-nfc 2883 |
This theorem is referenced by: nfeq1 2908 nfeq2 2910 nfne 3024 raleqf 3265 rexeqf 3266 reueq1f 3267 rmoeq1f 3268 rabeqf 3322 csbhypf 3685 sbceqg 4119 nffn 6140 nffo 6267 fvmptd3f 6449 mpteqb 6453 fvmptf 6455 eqfnfv2f 6470 dff13f 6668 ovmpt2s 6941 ov2gf 6942 ovmpt2dxf 6943 ovmpt2df 6949 eqerlem 7937 seqof2 13045 sumeq2ii 14614 sumss 14646 fsumadd 14661 fsummulc2 14707 fsumrelem 14730 prodeq1f 14829 prodeq2ii 14834 fprodmul 14881 fproddiv 14882 fprodle 14918 txcnp 21617 ptcnplem 21618 cnmpt11 21660 cnmpt21 21668 cnmptcom 21675 mbfeqalem 23600 mbflim 23626 itgeq1f 23729 itgeqa 23771 dvmptfsum 23929 ulmss 24342 leibpi 24860 o1cxp 24892 lgseisenlem2 25292 fmptcof2 29758 aciunf1lem 29763 sigapildsys 30526 bnj1316 31190 bnj1446 31412 bnj1447 31413 bnj1448 31414 bnj1519 31432 bnj1520 31433 bnj1529 31437 nosupbnd1 32158 subtr 32606 subtr2 32607 bj-sbeqALT 33193 poimirlem25 33739 iuneq2f 34268 mpt2bi123f 34276 mptbi12f 34280 dvdsrabdioph 37868 fphpd 37874 fvelrnbf 39668 refsum2cnlem1 39687 dffo3f 39855 elrnmptf 39858 disjrnmpt2 39866 disjinfi 39871 choicefi 39883 axccdom 39907 fvelimad 39949 uzublem 40147 fsumf1of 40301 fmuldfeq 40310 mccl 40325 climmulf 40331 climexp 40332 climsuse 40335 climrecf 40336 climaddf 40342 mullimc 40343 neglimc 40374 addlimc 40375 0ellimcdiv 40376 climeldmeqmpt 40395 climfveqmpt 40398 climfveqf 40407 climfveqmpt3 40409 climeldmeqf 40410 climeqf 40415 climeldmeqmpt3 40416 limsupubuzlem 40439 limsupequz 40450 dvnmptdivc 40648 dvmptfprod 40655 dvnprodlem1 40656 stoweidlem18 40730 stoweidlem31 40743 stoweidlem55 40767 stoweidlem59 40771 sge0f1o 41094 sge0iunmpt 41130 sge0reuz 41159 iundjiun 41172 hoicvrrex 41268 ovnhoilem1 41313 ovnlecvr2 41322 opnvonmbllem1 41344 vonioo 41394 vonicc 41397 sssmf 41445 smflim 41483 smfpimcclem 41511 smfpimcc 41512 ovmpt2rdxf 42619 |
Copyright terms: Public domain | W3C validator |