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 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 ⊢ Ⅎ 𝑥 𝐴
nfun.2 ⊢ Ⅎ 𝑥 𝐵
Assertion
nfunOLD ⊢ Ⅎ 𝑥 ( 𝐴 ∪ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
nfun.1 ⊢ Ⅎ 𝑥 𝐴
2
nfun.2 ⊢ Ⅎ 𝑥 𝐵
3
df-un ⊢ ( 𝐴 ∪ 𝐵 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 ) }
4
1
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5
2
nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
6
4 5
nfor ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 )
7
6
nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 ) }
8
3 7
nfcxfr ⊢ Ⅎ 𝑥 ( 𝐴 ∪ 𝐵 )