Metamath Proof Explorer


Theorem raluz

Description: Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005)

Ref Expression
Assertion raluz M n M φ n M n φ

Proof

Step Hyp Ref Expression
1 eluz1 M n M n M n
2 1 imbi1d M n M φ n M n φ
3 impexp n M n φ n M n φ
4 2 3 bitrdi M n M φ n M n φ
5 4 ralbidv2 M n M φ n M n φ