Metamath Proof Explorer

Theorem bj-axc14nf

Description: Proof of a version of axc14 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc14nf 
|- ( -. A. z z = x -> ( -. A. z z = y -> F/ z x e. y ) )

Proof

Step Hyp Ref Expression
1 bj-nfeel2 
 |-  ( -. A. z z = x -> F/ z x e. t )
2 elequ2 
 |-  ( t = y -> ( x e. t <-> x e. y ) )
3 1 2 bj-dvelimdv1 
 |-  ( -. A. z z = x -> ( -. A. z z = y -> F/ z x e. y ) )