Metamath Proof Explorer
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10Oct2016)


Ref 
Expression 

Hypothesis 
nfeq1.1 
$${\u22a2}\underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$ 

Assertion 
nfel1 
$${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{A}\in {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfeq1.1 
$${\u22a2}\underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$ 
2 

nfcv 
$${\u22a2}\underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{B}$$ 
3 
1 2

nfel 
$${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{A}\in {B}$$ 