Theorem bj-adjg1

Description: Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-adjg1	|- ( A e. V -> ( A u. { x } ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		uneq1	|- ( y = A -> ( y u. { x } ) = ( A u. { x } ) )
2	1	eleq1d	|- ( y = A -> ( ( y u. { x } ) e. _V <-> ( A u. { x } ) e. _V ) )
3		ax-bj-adj	|- A. y A. x E. z A. t ( t e. z <-> ( t e. y \/ t = x ) )
4	3	spi	|- A. x E. z A. t ( t e. z <-> ( t e. y \/ t = x ) )
5	4	spi	|- E. z A. t ( t e. z <-> ( t e. y \/ t = x ) )
6		bj-axadj	|- ( ( y u. { x } ) e. _V <-> E. z A. t ( t e. z <-> ( t e. y \/ t = x ) ) )
7	5 6	mpbir	|- ( y u. { x } ) e. _V
8	2 7	vtoclg	|- ( A e. V -> ( A u. { x } ) e. _V )