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 union of two classes nfun
Description: Bound-variable hypothesis builder for the union of classes.
(Contributed by NM , 15-Sep-2003) (Revised by Mario Carneiro , 14-Oct-2016) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN , 14-May-2025)
Ref
Expression
Hypotheses
nfun.1 ⊢ Ⅎ _ x A
nfun.2 ⊢ Ⅎ _ x B
Assertion
nfun ⊢ Ⅎ _ x A ∪ B
Proof
Step
Hyp
Ref
Expression
1
nfun.1 ⊢ Ⅎ _ x A
2
nfun.2 ⊢ Ⅎ _ x B
3
elun ⊢ y ∈ A ∪ B ↔ 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
3 6
nfxfr ⊢ Ⅎ x y ∈ A ∪ B
8
7
nfci ⊢ Ⅎ _ x A ∪ B