Theorem vsmext

Description: The universe is a standard model of the Axiom of Extensionality. (Contributed by BTernaryTau, 2-Oct-2026)

	Ref	Expression
Assertion	vsmext	|- _V |=. Ax-Ext

Proof

Step	Hyp	Ref	Expression
1		ralv	|- ( A. z e. _V ( z e. x <-> z e. y ) <-> A. z ( z e. x <-> z e. y ) )
2		ax-ext	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
3	1 2	sylbi	|- ( A. z e. _V ( z e. x <-> z e. y ) -> x = y )
4	3	rgen2w	|- A. x e. _V A. y e. _V ( A. z e. _V ( z e. x <-> z e. y ) -> x = y )
5		df-smext	|- ( _V |=. Ax-Ext <-> A. x e. _V A. y e. _V ( A. z e. _V ( z e. x <-> z e. y ) -> x = y ) )
6	4 5	mpbir	|- _V |=. Ax-Ext