Metamath Proof Explorer


Theorem sbc5ALT

Description: Alternate proof of sbc5 . This proof helps show how clelab works, since it is equivalent but shorter thanks to now-available library theorems like vtoclbg and isset . (Contributed by NM, 23-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbc5ALT [˙A / x]˙ φ x x = A φ

Proof

Step Hyp Ref Expression
1 sbcex [˙A / x]˙ φ A V
2 exsimpl x x = A φ x x = A
3 isset A V x x = A
4 2 3 sylibr x x = A φ A V
5 dfsbcq2 y = A y x φ [˙A / x]˙ φ
6 eqeq2 y = A x = y x = A
7 6 anbi1d y = A x = y φ x = A φ
8 7 exbidv y = A x x = y φ x x = A φ
9 sb5 y x φ x x = y φ
10 5 8 9 vtoclbg A V [˙A / x]˙ φ x x = A φ
11 1 4 10 pm5.21nii [˙A / x]˙ φ x x = A φ