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 vtocle
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM , 9-Sep-1993) Avoid df-clab . (Revised by Wolf Lammen , 31-May-2025)
Ref
Expression
Hypotheses
vtocle.1 |- A e. _V
vtocle.2 |- ( x = A -> ph )
Assertion
vtocle |- ph
Proof
Step
Hyp
Ref
Expression
1
vtocle.1 |- A e. _V
2
vtocle.2 |- ( x = A -> ph )
3
1
isseti |- E. x x = A
4
2 3
exlimiiv |- ph