Theorem prdsbasex

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

	Ref	Expression
Hypothesis	prdsbasex.b	|- B = X_ x e. dom R ( Base ` ( R ` x ) )
Assertion	prdsbasex	|- B e. _V

Proof

Step	Hyp	Ref	Expression
1		prdsbasex.b	|- B = X_ x e. dom R ( Base ` ( R ` x ) )
2		ixpexg	|- ( A. x e. dom R ( Base ` ( R ` x ) ) e. _V -> X_ x e. dom R ( Base ` ( R ` x ) ) e. _V )
3		fvexd	|- ( x e. dom R -> ( Base ` ( R ` x ) ) e. _V )
4	2 3	mprg	|- X_ x e. dom R ( Base ` ( R ` x ) ) e. _V
5	1 4	eqeltri	|- B e. _V