Theorem uniclaxun

Description: A class that is closed under the union operation models the Axiom of Union ax-un . Lemma II.2.4(5) of Kunen2 p. 111. (Contributed by Eric Schmidt, 1-Oct-2025)

	Ref	Expression
Assertion	uniclaxun	|- ( A. x e. M U. x e. M -> A. x e. M E. y e. M A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		rexex	|- ( E. w e. M ( z e. w /\ w e. x ) -> E. w ( z e. w /\ w e. x ) )
2		eluni	|- ( z e. U. x <-> E. w ( z e. w /\ w e. x ) )
3	1 2	sylibr	|- ( E. w e. M ( z e. w /\ w e. x ) -> z e. U. x )
4	3	rgenw	|- A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. U. x )
5		eleq2	|- ( y = U. x -> ( z e. y <-> z e. U. x ) )
6	5	imbi2d	|- ( y = U. x -> ( ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) <-> ( E. w e. M ( z e. w /\ w e. x ) -> z e. U. x ) ) )
7	6	ralbidv	|- ( y = U. x -> ( A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) <-> A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. U. x ) ) )
8	7	rspcev	|- ( ( U. x e. M /\ A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. U. x ) ) -> E. y e. M A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) )
9	4 8	mpan2	|- ( U. x e. M -> E. y e. M A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) )
10	9	ralimi	|- ( A. x e. M U. x e. M -> A. x e. M E. y e. M A. z e. M ( E. w e. M ( z e. w /\ w e. x ) -> z e. y ) )