Metamath Proof Explorer


Theorem bj-axc14

Description: Alternate proof of axc14 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bj-axc14nf
 |-  ( -. A. z z = x -> ( -. A. z z = y -> F/ z x e. y ) )
2 nf5r
 |-  ( F/ z x e. y -> ( x e. y -> A. z x e. y ) )
3 2 a1i
 |-  ( -. A. z z = x -> ( F/ z x e. y -> ( x e. y -> A. z x e. y ) ) )
4 1 3 syld
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )