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

Metamath Proof Explorer

Theorem iunex

Description: The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B , which can be read informally as B ( x ) . (Contributed by NM, 13-Oct-2003)

	Ref	Expression
Hypotheses	iunex.1	⊢ 𝐴 ∈ V
	iunex.2	⊢ 𝐵 ∈ V
Assertion	iunex	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V

Proof

Step	Hyp	Ref	Expression
1		iunex.1	⊢ 𝐴 ∈ V
2		iunex.2	⊢ 𝐵 ∈ V
3	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V
4		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
5	1 3 4	mp2an	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V