Metamath Proof Explorer

Theorem 2rexbii

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995)

Ref Expression
Hypothesis rexbii.1 
|- ( ph <-> ps )
Assertion 2rexbii 
|- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )

Proof

Step Hyp Ref Expression
1 rexbii.1 
 |-  ( ph <-> ps )
2 1 rexbii 
 |-  ( E. y e. B ph <-> E. y e. B ps )
3 2 rexbii 
 |-  ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )