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

Metamath Proof Explorer

Theorem iinexd

Description: The existence of an indexed union. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	iinexd.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	iinexd.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
Assertion	iinexd	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		iinexd.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2		iinexd.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
3		iinexg	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )