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

Metamath Proof Explorer

Theorem nfunOLD

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

Ref Expression
Hypotheses nfun.1 ⊢ Ⅎ _ x A
nfun.2 ⊢ Ⅎ _ x B
Assertion nfunOLD ⊢ Ⅎ _ x A ∪ B

Proof

Step Hyp Ref Expression
1 nfun.1 ⊢ Ⅎ _ x A
2 nfun.2 ⊢ Ⅎ _ x B
3 df-un ⊢ A ∪ B = y | y ∈ A ∨ y ∈ B
4 1 nfcri ⊢ Ⅎ x y ∈ A
5 2 nfcri ⊢ Ⅎ x y ∈ B
6 4 5 nfor ⊢ Ⅎ x y ∈ A ∨ y ∈ B
7 6 nfab ⊢ Ⅎ _ x y | y ∈ A ∨ y ∈ B
8 3 7 nfcxfr ⊢ Ⅎ _ x A ∪ B