This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Proper substitution of classes for sets sbciegft
Description: Conversion of implicit substitution to explicit class substitution,
using a bound-variable hypothesis instead of distinct variables.
(Closed theorem version of sbciegf .) (Contributed by NM , 10-Nov-2005) (Revised by Mario Carneiro , 13-Oct-2016) (Proof
shortened by SN , 14-May-2025)
Ref
Expression
Assertion
sbciegft |- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )
Proof
Step
Hyp
Ref
Expression
1
sbc6g |- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
2
1
3ad2ant1 |- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
3
ceqsalt |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
4
3
3comr |- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A. x ( x = A -> ph ) <-> ps ) )
5
2 4
bitrd |- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )