Theorem prdsbasex

Description: Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015)

	Ref	Expression
Hypothesis	prdsbasex.b	⊢ 𝐵 = X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
Assertion	prdsbasex	⊢ 𝐵 ∈ V

Proof

Step	Hyp	Ref	Expression
1		prdsbasex.b	⊢ 𝐵 = X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
2		ixpexg	⊢ ( ∀ 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V → X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
3		fvexd	⊢ ( 𝑥 ∈ dom 𝑅 → ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
4	2 3	mprg	⊢ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V
5	1 4	eqeltri	⊢ 𝐵 ∈ V