Theorem vsmext

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

	Ref	Expression
Assertion	vsmext	Could not format assertion : No typesetting found for |- _V |=. Ax-Ext with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ralv	$$⊢\forall z\in \mathrm{V}\left(z\in x\leftrightarrow z\in y\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow z\in y\right)$$
2		ax-ext	$$⊢\forall z\left(z\in x\leftrightarrow z\in y\right)\to x=y$$
3	1 2	sylbi	$$⊢\forall z\in \mathrm{V}\left(z\in x\leftrightarrow z\in y\right)\to x=y$$
4	3	rgen2w	$$⊢\forall x\in \mathrm{V}\forall y\in \mathrm{V}\left(\forall z\in \mathrm{V}\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$
5		df-smext	Could not format ( _V |=. Ax-Ext <-> A. x e. _V A. y e. _V ( A. z e. _V ( z e. x <-> z e. y ) -> x = y ) ) : No typesetting found for |- ( _V |=. Ax-Ext <-> A. x e. _V A. y e. _V ( A. z e. _V ( z e. x <-> z e. y ) -> x = y ) ) with typecode |-
6	4 5	mpbir	Could not format _V |=. Ax-Ext : No typesetting found for |- _V |=. Ax-Ext with typecode |-