![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfel2 | Structured version Visualization version GIF 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 2903 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfel 2917 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1785 ∈ wcel 2106 Ⅎwnfc 2883 |
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-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
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 2724 df-clel 2810 df-nfc 2885 |
This theorem is referenced by: elabgtOLD 3662 elabgOLD 3666 0nelopabOLD 5567 eliunxp 5835 opeliunxp2 5836 tz6.12f 6914 riotaxfrd 7396 opeliunxp2f 8191 cbvixp 8904 boxcutc 8931 ixpiunwdom 9581 rankidb 9791 rankuni2b 9844 acni2 10037 ac6c4 10472 iundom2g 10531 tskuni 10774 reuccatpfxs1 14693 gsumcom2 19837 gsummatr01lem4 22151 ptclsg 23110 cnextfvval 23560 prdsdsf 23864 nnindf 32012 gsumpart 32194 nsgqusf1olem1 32512 nsgqusf1olem3 32514 bnj1463 34054 fineqvrep 34083 ptrest 36475 sdclem1 36599 eqrelf 37111 binomcxplemnotnn0 43100 eliin2f 43778 stoweidlem26 44728 stoweidlem36 44738 stoweidlem46 44748 stoweidlem51 44753 finfdm 45548 eliunxp2 46962 setrec1 47689 |
Copyright terms: Public domain | W3C validator |