![]() |
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 2913 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfel 2926 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1856 ∈ wcel 2145 Ⅎwnfc 2900 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-cleq 2764 df-clel 2767 df-nfc 2902 |
This theorem is referenced by: elabgt 3498 opelopabsb 5118 eliunxp 5398 opeliunxp2 5399 tz6.12f 6353 riotaxfrd 6785 0neqopab 6845 opeliunxp2f 7488 cbvixp 8079 boxcutc 8105 ixpiunwdom 8652 rankidb 8827 rankuni2b 8880 acni2 9069 ac6c4 9505 iundom2g 9564 tskuni 9807 reuccats1 13689 gsumcom2 18581 gsummatr01lem4 20683 ptclsg 21639 cnextfvval 22089 prdsdsf 22392 nnindf 29905 bnj1463 31461 ptrest 33741 sdclem1 33871 eqrelf 34363 binomcxplemnotnn0 39081 eliin2f 39808 stoweidlem26 40760 stoweidlem36 40770 stoweidlem46 40780 stoweidlem51 40785 eliunxp2 42640 setrec1 42966 |
Copyright terms: Public domain | W3C validator |