![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfel2 | Structured version Visualization version Unicode version |
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
nfeq2.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfel2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2612 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfeq2.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | nfel 2624 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-cleq 2464 df-clel 2467 df-nfc 2601 |
This theorem is referenced by: elabgt 3170 opelopabsb 4711 eliunxp 4977 opeliunxp2 4978 tz6.12f 5897 riotaxfrd 6300 0neqopab 6353 opeliunxp2f 6975 cbvixp 7557 boxcutc 7583 ixpiunwdom 8124 rankidb 8289 rankuni2b 8342 acni2 8495 ac6c4 8929 iundom2g 8983 tskuni 9226 gsumcom2 17685 gsummatr01lem4 19760 ptclsg 20707 cnextfvval 21158 prdsdsf 21460 nnindf 28457 bnj1463 29936 ptrest 32003 sdclem1 32136 binomcxplemnotnn0 36775 stoweidlem26 37998 stoweidlem36 38009 stoweidlem46 38019 stoweidlem51 38024 eliunxp2 40623 |
Copyright terms: Public domain | W3C validator |