![]() |
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 2934 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfel 2946 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1827 ∈ wcel 2107 Ⅎwnfc 2919 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-cleq 2770 df-clel 2774 df-nfc 2921 |
This theorem is referenced by: elabgt 3553 elabg 3556 opelopabsb 5222 eliunxp 5505 opeliunxp2 5506 tz6.12f 6470 riotaxfrd 6914 0neqopab 6975 opeliunxp2f 7618 cbvixp 8211 boxcutc 8237 ixpiunwdom 8785 rankidb 8960 rankuni2b 9013 acni2 9202 ac6c4 9638 iundom2g 9697 tskuni 9940 reuccats1OLD 13848 reuccatpfxs1 13883 gsumcom2 18760 gsummatr01lem4 20870 ptclsg 21827 cnextfvval 22277 prdsdsf 22580 nnindf 30129 bnj1463 31722 ptrest 34034 sdclem1 34163 eqrelf 34655 binomcxplemnotnn0 39511 eliin2f 40216 stoweidlem26 41170 stoweidlem36 41180 stoweidlem46 41190 stoweidlem51 41195 eliunxp2 43127 setrec1 43543 |
Copyright terms: Public domain | W3C validator |