Metamath Proof Explorer


Theorem ralimralim

Description: Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion ralimralim
|- ( A. x e. A ph -> A. x e. A ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 nfra1
 |-  F/ x A. x e. A ph
2 rspa
 |-  ( ( A. x e. A ph /\ x e. A ) -> ph )
3 ax-1
 |-  ( ph -> ( ps -> ph ) )
4 2 3 syl
 |-  ( ( A. x e. A ph /\ x e. A ) -> ( ps -> ph ) )
5 4 ex
 |-  ( A. x e. A ph -> ( x e. A -> ( ps -> ph ) ) )
6 1 5 ralrimi
 |-  ( A. x e. A ph -> A. x e. A ( ps -> ph ) )