This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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