Metamath Proof Explorer


Theorem ceqsalALT

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. Shorter proof uses df-clab . (Contributed by NM, 18-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ceqsal.1
|- F/ x ps
ceqsal.2
|- A e. _V
ceqsal.3
|- ( x = A -> ( ph <-> ps ) )
Assertion ceqsalALT
|- ( A. x ( x = A -> ph ) <-> ps )

Proof

Step Hyp Ref Expression
1 ceqsal.1
 |-  F/ x ps
2 ceqsal.2
 |-  A e. _V
3 ceqsal.3
 |-  ( x = A -> ( ph <-> ps ) )
4 1 3 ceqsalg
 |-  ( A e. _V -> ( A. x ( x = A -> ph ) <-> ps ) )
5 2 4 ax-mp
 |-  ( A. x ( x = A -> ph ) <-> ps )