Metamath Proof Explorer

Theorem r19.23v

Description: Restricted quantifier version of 19.23v . Version of r19.23 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 con34b 
 |-  ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )
2 1 ralbii 
 |-  ( A. x e. A ( ph -> ps ) <-> A. x e. A ( -. ps -> -. ph ) )
3 r19.21v 
 |-  ( A. x e. A ( -. ps -> -. ph ) <-> ( -. ps -> A. x e. A -. ph ) )
4 dfrex2 
 |-  ( E. x e. A ph <-> -. A. x e. A -. ph )
5 4 imbi1i 
 |-  ( ( E. x e. A ph -> ps ) <-> ( -. A. x e. A -. ph -> ps ) )
6 con1b 
 |-  ( ( -. A. x e. A -. ph -> ps ) <-> ( -. ps -> A. x e. A -. ph ) )
7 5 6 bitr2i 
 |-  ( ( -. ps -> A. x e. A -. ph ) <-> ( E. x e. A ph -> ps ) )
8 2 3 7 3bitri 
 |-  ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )