Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Negated equality and membership
Negated membership
nfneld
Metamath Proof Explorer
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
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ∉ 𝐵 )