Metamath Proof Explorer


Theorem 2rspcedvdw

Description: Double application of rspcedvdw . (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses 2rspcedvdw.1
|- ( x = A -> ( ps <-> ch ) )
2rspcedvdw.2
|- ( y = B -> ( ch <-> th ) )
2rspcedvdw.a
|- ( ph -> A e. X )
2rspcedvdw.b
|- ( ph -> B e. Y )
2rspcedvdw.3
|- ( ph -> th )
Assertion 2rspcedvdw
|- ( ph -> E. x e. X E. y e. Y ps )

Proof

Step Hyp Ref Expression
1 2rspcedvdw.1
 |-  ( x = A -> ( ps <-> ch ) )
2 2rspcedvdw.2
 |-  ( y = B -> ( ch <-> th ) )
3 2rspcedvdw.a
 |-  ( ph -> A e. X )
4 2rspcedvdw.b
 |-  ( ph -> B e. Y )
5 2rspcedvdw.3
 |-  ( ph -> th )
6 1 2 rspc2ev
 |-  ( ( A e. X /\ B e. Y /\ th ) -> E. x e. X E. y e. Y ps )
7 3 4 5 6 syl3anc
 |-  ( ph -> E. x e. X E. y e. Y ps )