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 The universal class ceqsalg
Description: A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. For an alternate
proof, see ceqsalgALT . (Contributed by NM , 29-Oct-2003) (Proof
shortened by BJ , 29-Sep-2019)
Ref
Expression
Hypotheses
ceqsalg.1 |- F/ x ps
ceqsalg.2 |- ( x = A -> ( ph <-> ps ) )
Assertion
ceqsalg |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Proof
Step
Hyp
Ref
Expression
1
ceqsalg.1 |- F/ x ps
2
ceqsalg.2 |- ( x = A -> ( ph <-> ps ) )
3
2
ax-gen |- A. x ( x = A -> ( ph <-> ps ) )
4
ceqsalt |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
5
1 3 4
mp3an12 |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )