Metamath Proof Explorer


Theorem nfeld

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

Ref Expression
Hypotheses nfeqd.1 φ _ x A
nfeqd.2 φ _ x B
Assertion nfeld φ x A B

Proof

Step Hyp Ref Expression
1 nfeqd.1 φ _ x A
2 nfeqd.2 φ _ x B
3 dfclel A B y y = A y B
4 nfv y φ
5 nfcvd φ _ x y
6 5 1 nfeqd φ x y = A
7 2 nfcrd φ x y B
8 6 7 nfand φ x y = A y B
9 4 8 nfexd φ x y y = A y B
10 3 9 nfxfrd φ x A B