Metamath Proof Explorer

Theorem rexbiOLD

Description: Obsolete version of rexbi as of 31-Oct-2024. (Contributed by Scott Fenton, 7-Aug-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ralbi 
 |-  ( A. x e. A ( -. ph <-> -. ps ) -> ( A. x e. A -. ph <-> A. x e. A -. ps ) )
2 1 notbid 
 |-  ( A. x e. A ( -. ph <-> -. ps ) -> ( -. A. x e. A -. ph <-> -. A. x e. A -. ps ) )
3 notbi 
 |-  ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
4 3 ralbii 
 |-  ( A. x e. A ( ph <-> ps ) <-> A. x e. A ( -. ph <-> -. ps ) )
5 dfrex2 
 |-  ( E. x e. A ph <-> -. A. x e. A -. ph )
6 dfrex2 
 |-  ( E. x e. A ps <-> -. A. x e. A -. ps )
7 5 6 bibi12i 
 |-  ( ( E. x e. A ph <-> E. x e. A ps ) <-> ( -. A. x e. A -. ph <-> -. A. x e. A -. ps ) )
8 2 4 7 3imtr4i 
 |-  ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )