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

Metamath Proof Explorer

Theorem rexbi

Description: Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024) (Proof shortened by Wolf Lammen, 3-Nov-2024)

Ref Expression
Assertion rexbi 
|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 biimp 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
2 1 ralimi 
 |-  ( A. x e. A ( ph <-> ps ) -> A. x e. A ( ph -> ps ) )
3 rexim 
 |-  ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
4 2 3 syl 
 |-  ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
5 biimpr 
 |-  ( ( ph <-> ps ) -> ( ps -> ph ) )
6 5 ralimi 
 |-  ( A. x e. A ( ph <-> ps ) -> A. x e. A ( ps -> ph ) )
7 rexim 
 |-  ( A. x e. A ( ps -> ph ) -> ( E. x e. A ps -> E. x e. A ph ) )
8 6 7 syl 
 |-  ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ps -> E. x e. A ph ) )
9 4 8 impbid 
 |-  ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )