Metamath Proof Explorer

Theorem wl-ax11-lem7

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem7 
|- ( A. x ( -. A. x x = y /\ ph ) <-> ( -. A. x x = y /\ A. x ph ) )

Proof

Step Hyp Ref Expression
1 nfna1 
 |-  F/ x -. A. x x = y
2 1 19.28 
 |-  ( A. x ( -. A. x x = y /\ ph ) <-> ( -. A. x x = y /\ A. x ph ) )