vsmrep

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

		Ref	Expression
	Assertion	vsmrep	Could not format assertion : No typesetting found for \|- _V \|=. Ax-Rep* with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		df-smrep	Could not format ( _V \|=. Ax-Rep* <-> A. f A. x e. _V ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) : No typesetting found for \|- ( _V \|=. Ax-Rep* <-> A. f A. x e. _V ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode \|-
2		ax-rep	$⊢ \forall w \exists y \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \to \exists y \forall z (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
3		ralv	$⊢ \forall w \in V \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \forall w \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
4		rexv	$⊢ \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \exists y \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
5		ralv	$⊢ \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
6	5	exbii	$⊢ \exists y \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \exists y \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
7	4 6	bitri	$⊢ \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \exists y \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
8	7	albii	$⊢ \forall w \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \forall w \exists y \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
9	3 8	bitri	$⊢ \forall w \in V \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \leftrightarrow \forall w \exists y \forall z (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
10		rexv	$⊢ \exists y \in V \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \exists y \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
11		ralv	$⊢ \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \forall z (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
12		rexv	$⊢ \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)) \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))$
13	12	bibi2i	$⊢ (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
14	13	albii	$⊢ \forall z (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \forall z (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
15	11 14	bitri	$⊢ \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \forall z (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
16	15	exbii	$⊢ \exists y \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \exists y \forall z (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
17	10 16	bitri	$⊢ \exists y \in V \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \exists y \forall z (z \in y \leftrightarrow \exists w (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
18	2 9 17	3imtr4i	$⊢ \forall w \in V \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \to \exists y \in V \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
19	18	rgenw	$⊢ \forall x \in V (\forall w \in V \exists y \in V \forall z \in V (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \to \exists y \in V \forall z \in V (z \in y \leftrightarrow \exists w \in V (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))))$
20	1 19	mpgbir	Could not format _V \|=. Ax-Rep* : No typesetting found for \|- _V \|=. Ax-Rep* with typecode \|-

Metamath Proof Explorer

Theorem vsmrep

Proof