Metamath Proof Explorer


Theorem eq0rdvALT

Description: Alternate proof of eq0rdv . Shorter, but requiring df-clel , ax-8 . (Contributed by NM, 11-Jul-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eq0rdvALT.1 φ¬xA
Assertion eq0rdvALT φA=

Proof

Step Hyp Ref Expression
1 eq0rdvALT.1 φ¬xA
2 1 pm2.21d φxAx
3 2 ssrdv φA
4 ss0 AA=
5 3 4 syl φA=