Metamath Proof Explorer


Theorem bj-nnflemea

Description: One of four lemmas for nonfreeness: antecedent expressed with existential quantifier and consequent expressed with universal quantifier. (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnflemea x y φ φ y x φ x φ

Proof

Step Hyp Ref Expression
1 bj-19.12 y x φ x y φ
2 alim x y φ φ x y φ x φ
3 1 2 syl5 x y φ φ y x φ x φ