Metamath Proof Explorer


Theorem dral1ALT

Description: Alternate proof of dral1 , shorter but requiring ax-11 . (Contributed by NM, 24-Nov-1994) (Proof shortened by Wolf Lammen, 22-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis dral1.1
|- ( A. x x = y -> ( ph <-> ps ) )
Assertion dral1ALT
|- ( A. x x = y -> ( A. x ph <-> A. y ps ) )

Proof

Step Hyp Ref Expression
1 dral1.1
 |-  ( A. x x = y -> ( ph <-> ps ) )
2 1 dral2
 |-  ( A. x x = y -> ( A. x ph <-> A. x ps ) )
3 axc11
 |-  ( A. x x = y -> ( A. x ps -> A. y ps ) )
4 axc11r
 |-  ( A. x x = y -> ( A. y ps -> A. x ps ) )
5 3 4 impbid
 |-  ( A. x x = y -> ( A. x ps <-> A. y ps ) )
6 2 5 bitrd
 |-  ( A. x x = y -> ( A. x ph <-> A. y ps ) )