Metamath Proof Explorer


Theorem ixpssixp

Description: Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ixpssixp.1 𝑥 𝜑
ixpssixp.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
Assertion ixpssixp ( 𝜑X 𝑥𝐴 𝐵X 𝑥𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 ixpssixp.1 𝑥 𝜑
2 ixpssixp.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
3 2 ex ( 𝜑 → ( 𝑥𝐴𝐵𝐶 ) )
4 1 3 ralrimi ( 𝜑 → ∀ 𝑥𝐴 𝐵𝐶 )
5 ss2ixp ( ∀ 𝑥𝐴 𝐵𝐶X 𝑥𝐴 𝐵X 𝑥𝐴 𝐶 )
6 4 5 syl ( 𝜑X 𝑥𝐴 𝐵X 𝑥𝐴 𝐶 )