| 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 2905 | . 2 ⊢ Ⅎ𝑥𝐴 | |
| 2 | nfeq2.1 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 3 | 1, 2 | nfel 2920 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-clel 2816 df-nfc 2892 |
| This theorem is referenced by: eliunxp 5848 opeliunxp2 5849 tz6.12f 6932 riotaxfrd 7422 opeliunxp2f 8235 cbvixp 8954 boxcutc 8981 ixpiunwdom 9630 rankidb 9840 rankuni2b 9893 acni2 10086 ac6c4 10521 iundom2g 10580 tskuni 10823 reuccatpfxs1 14785 gsumcom2 19993 gsummatr01lem4 22664 ptclsg 23623 cnextfvval 24073 prdsdsf 24377 nnindf 32821 gsumpart 33060 nsgqusf1olem1 33441 nsgqusf1olem3 33443 bnj1463 35069 fineqvrep 35109 ptrest 37626 sdclem1 37750 eqrelf 38256 binomcxplemnotnn0 44375 eliin2f 45109 stoweidlem26 46041 stoweidlem36 46051 stoweidlem46 46061 stoweidlem51 46066 sge0f1o 46397 finfdm 46861 eliunxp2 48250 setrec1 49210 |
| Copyright terms: Public domain | W3C validator |