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 2899 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfel 2913 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1790 ∈ wcel 2113 Ⅎwnfc 2879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-cleq 2730 df-clel 2811 df-nfc 2881 |
This theorem is referenced by: elabgt 3565 elabg 3570 0nelopab 5417 eliunxp 5674 opeliunxp2 5675 tz6.12f 6692 riotaxfrd 7156 opeliunxp2f 7898 cbvixp 8517 boxcutc 8544 ixpiunwdom 9120 rankidb 9295 rankuni2b 9348 acni2 9539 ac6c4 9974 iundom2g 10033 tskuni 10276 reuccatpfxs1 14191 gsumcom2 19207 gsummatr01lem4 21402 ptclsg 22359 cnextfvval 22809 prdsdsf 23113 nnindf 30700 gsumpart 30884 nsgqusf1olem1 31162 nsgqusf1olem3 31164 bnj1463 32598 fineqvrep 32627 ptrest 35388 sdclem1 35513 eqrelf 36007 binomcxplemnotnn0 41496 eliin2f 42176 stoweidlem26 43093 stoweidlem36 43103 stoweidlem46 43113 stoweidlem51 43118 eliunxp2 45187 setrec1 45834 |
Copyright terms: Public domain | W3C validator |