Metamath Proof Explorer

Theorem 19.12

Description: Theorem 19.12 of Margaris p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv and r19.12sn . (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 3-Jan-2018)

Ref Expression
Assertion 19.12 x y φ y x φ


Step Hyp Ref Expression
1 nfa1 y y φ
2 1 nfex y x y φ
3 sp y φ φ
4 3 eximi x y φ x φ
5 2 4 alrimi x y φ y x φ