Metamath Proof Explorer

Theorem sbhb

Description: Two ways of expressing " x is (effectively) not free in ph ". Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-May-2009) (New usage is discouraged.)

Ref Expression
Assertion sbhb φ x φ y φ y x φ


Step Hyp Ref Expression
1 nfv y φ
2 1 sb8 x φ y y x φ
3 2 imbi2i φ x φ φ y y x φ
4 19.21v y φ y x φ φ y y x φ
5 3 4 bitr4i φ x φ y φ y x φ