Metamath Proof Explorer

Theorem nfeld

Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016)

Ref Expression
Hypotheses nfeqd.1 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfeqd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfeld ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in {B}$

Proof

Step Hyp Ref Expression
1 nfeqd.1 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfeqd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 dfclel ${⊢}{A}\in {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {y}\in {B}\right)$
4 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 nfcvd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
6 5 1 nfeqd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={A}$
7 2 nfcrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
8 6 7 nfand ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {y}\in {B}\right)$
9 4 8 nfexd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {y}\in {B}\right)$
10 3 9 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in {B}$