This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The difference, union, and intersection of two classes The difference of two classes nfdif
Description: Bound-variable hypothesis builder for class difference. (Contributed by NM , 3-Dec-2003) (Revised by Mario Carneiro , 13-Oct-2016) Avoid
ax-10 , ax-11 , ax-12 . (Revised by SN , 14-May-2025)
Ref
Expression
Hypotheses
nfdif.1 ⊢ Ⅎ 𝑥 𝐴
nfdif.2 ⊢ Ⅎ 𝑥 𝐵
Assertion
nfdif ⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
nfdif.1 ⊢ Ⅎ 𝑥 𝐴
2
nfdif.2 ⊢ Ⅎ 𝑥 𝐵
3
eldif ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
4
1
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5
2
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
6
5
nfn ⊢ Ⅎ 𝑥 ¬ 𝑦 ∈ 𝐵
7
4 6
nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 )
8
3 7
nfxfr ⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝐴 ∖ 𝐵 )
9
8
nfci ⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐵 )