This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2rmorex

Description: Double restricted quantification with "at most one", analogous to 2moex . (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2rmorex 
|- ( E* x e. A E. y e. B ph -> A. y e. B E* x e. A ph )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ y A
2 nfre1 
 |-  F/ y E. y e. B ph
3 1 2 nfrmow 
 |-  F/ y E* x e. A E. y e. B ph
4 rmoim 
 |-  ( A. x e. A ( ph -> E. y e. B ph ) -> ( E* x e. A E. y e. B ph -> E* x e. A ph ) )
5 rspe 
 |-  ( ( y e. B /\ ph ) -> E. y e. B ph )
6 5 ex 
 |-  ( y e. B -> ( ph -> E. y e. B ph ) )
7 6 ralrimivw 
 |-  ( y e. B -> A. x e. A ( ph -> E. y e. B ph ) )
8 4 7 syl11 
 |-  ( E* x e. A E. y e. B ph -> ( y e. B -> E* x e. A ph ) )
9 3 8 ralrimi 
 |-  ( E* x e. A E. y e. B ph -> A. y e. B E* x e. A ph )