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 Indexed union and intersection nfiu1OLD
Description: Obsolete version of nfiu1 as of 14-May-2025. (Contributed by NM , 12-Oct-2003) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
nfiu1OLD ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
Proof
Step
Hyp
Ref
Expression
1
df-iun ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
2
nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3
2
nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
4
1 3
nfcxfr ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵