Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfeq2 | GIF version |
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
nfeq2.1 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfeq2 | ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2279 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfeq 2287 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: = wceq 1331 Ⅎwnf 1436 Ⅎwnfc 2266 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-cleq 2130 df-clel 2133 df-nfc 2268 |
This theorem is referenced by: issetf 2688 eqvincf 2805 csbhypf 3033 nfpr 3568 intab 3795 nfmpt 4015 cbvmptf 4017 cbvmpt 4018 repizf2 4081 moop2 4168 eusvnf 4369 elrnmpt1 4785 fmptco 5579 elabrex 5652 nfmpo 5833 cbvmpox 5842 ovmpodxf 5889 fmpox 6091 f1od2 6125 nfrecs 6197 erovlem 6514 xpf1o 6731 mapxpen 6735 mkvprop 7025 lble 8698 nfsum1 11118 nfsum 11119 zsumdc 11146 fsum3 11149 fsum3cvg2 11156 fsum2dlemstep 11196 mertenslem2 11298 nfcprod1 11316 nfcprod 11317 ctiunctlemfo 11941 ellimc3apf 12787 |
Copyright terms: Public domain | W3C validator |