Metamath Proof Explorer


Theorem bj-ralvw

Description: A weak version of ralv not using ax-ext (nor df-cleq , df-clel , df-v ), and only core FOL axioms. See also bj-rexvw . The analogues for reuv and rmov are not proved. (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-ralvw.1
|- ps
Assertion bj-ralvw
|- ( A. x e. { y | ps } ph <-> A. x ph )

Proof

Step Hyp Ref Expression
1 bj-ralvw.1
 |-  ps
2 df-ral
 |-  ( A. x e. { y | ps } ph <-> A. x ( x e. { y | ps } -> ph ) )
3 1 vexw
 |-  x e. { y | ps }
4 3 a1bi
 |-  ( ph <-> ( x e. { y | ps } -> ph ) )
5 4 albii
 |-  ( A. x ph <-> A. x ( x e. { y | ps } -> ph ) )
6 2 5 bitr4i
 |-  ( A. x e. { y | ps } ph <-> A. x ph )