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 2977 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfel 2992 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1780 ∈ wcel 2110 Ⅎwnfc 2961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-cleq 2814 df-clel 2893 df-nfc 2963 |
This theorem is referenced by: elabgt 3662 elabg 3665 opelopabsb 5416 0nelopab 5451 eliunxp 5707 opeliunxp2 5708 tz6.12f 6693 riotaxfrd 7147 opeliunxp2f 7875 cbvixp 8477 boxcutc 8504 ixpiunwdom 9054 rankidb 9228 rankuni2b 9281 acni2 9471 ac6c4 9902 iundom2g 9961 tskuni 10204 reuccatpfxs1 14108 gsumcom2 19094 gsummatr01lem4 21266 ptclsg 22222 cnextfvval 22672 prdsdsf 22976 nnindf 30534 bnj1463 32327 ptrest 34890 sdclem1 35017 eqrelf 35516 binomcxplemnotnn0 40686 eliin2f 41368 stoweidlem26 42310 stoweidlem36 42320 stoweidlem46 42330 stoweidlem51 42335 eliunxp2 44381 setrec1 44793 |
Copyright terms: Public domain | W3C validator |