Metamath Proof Explorer


Theorem nfneld

Description: Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011) (Revised by Mario Carneiro, 7-Oct-2016)

Ref Expression
Hypotheses nfneld.1 ( 𝜑 𝑥 𝐴 )
nfneld.2 ( 𝜑 𝑥 𝐵 )
Assertion nfneld ( 𝜑 → Ⅎ 𝑥 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 nfneld.1 ( 𝜑 𝑥 𝐴 )
2 nfneld.2 ( 𝜑 𝑥 𝐵 )
3 df-nel ( 𝐴𝐵 ↔ ¬ 𝐴𝐵 )
4 1 2 nfeld ( 𝜑 → Ⅎ 𝑥 𝐴𝐵 )
5 4 nfnd ( 𝜑 → Ⅎ 𝑥 ¬ 𝐴𝐵 )
6 3 5 nfxfrd ( 𝜑 → Ⅎ 𝑥 𝐴𝐵 )