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

Metamath Proof Explorer

Theorem nfdifOLD

Description: Obsolete version of nfdif as of 14-May-2025. (Contributed by NM, 3-Dec-2003) (Revised by Mario Carneiro, 13-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nfdif.1 ⊢ Ⅎ _ x A
nfdif.2 ⊢ Ⅎ _ x B
Assertion nfdifOLD ⊢ Ⅎ _ x A ∖ B

Proof

Step Hyp Ref Expression
1 nfdif.1 ⊢ Ⅎ _ x A
2 nfdif.2 ⊢ Ⅎ _ x B
3 dfdif2 ⊢ A ∖ B = y ∈ A | ¬ y ∈ B
4 2 nfcri ⊢ Ⅎ x y ∈ B
5 4 nfn ⊢ Ⅎ x ¬ y ∈ B
6 5 1 nfrabw ⊢ Ⅎ _ x y ∈ A | ¬ y ∈ B
7 3 6 nfcxfr ⊢ Ⅎ _ x A ∖ B