Metamath Proof Explorer


Theorem nfeld

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

Ref Expression
Hypotheses nfeqd.1
|- ( ph -> F/_ x A )
nfeqd.2
|- ( ph -> F/_ x B )
Assertion nfeld
|- ( ph -> F/ x A e. B )

Proof

Step Hyp Ref Expression
1 nfeqd.1
 |-  ( ph -> F/_ x A )
2 nfeqd.2
 |-  ( ph -> F/_ x B )
3 dfclel
 |-  ( A e. B <-> E. y ( y = A /\ y e. B ) )
4 nfv
 |-  F/ y ph
5 nfcvd
 |-  ( ph -> F/_ x y )
6 5 1 nfeqd
 |-  ( ph -> F/ x y = A )
7 2 nfcrd
 |-  ( ph -> F/ x y e. B )
8 6 7 nfand
 |-  ( ph -> F/ x ( y = A /\ y e. B ) )
9 4 8 nfexd
 |-  ( ph -> F/ x E. y ( y = A /\ y e. B ) )
10 3 9 nfxfrd
 |-  ( ph -> F/ x A e. B )