Theorem elxpcbasex1

Description: A non-empty base set of the product category indicates the existence of the first factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025) (Proof shortened by SN, 15-Oct-2025)

	Ref	Expression
Hypotheses	elxpcbasex1.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	elxpcbasex1	⊢ ( 𝜑 → 𝐶 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elxpcbasex1.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		reldmxpc	⊢ Rel dom ×c
5	1 2 4	strov2rcl	⊢ ( 𝑋 ∈ 𝐵 → 𝐶 ∈ V )
6	3 5	syl	⊢ ( 𝜑 → 𝐶 ∈ V )