Theorem vvin

Description: Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 . (Contributed by BJ, 12-Jul-2026)

	Ref	Expression
Assertion	vvin	|- ( ( A = _V /\ B = _V ) <-> ( A i^i B ) = _V )

Proof

Step	Hyp	Ref	Expression
1		ineq12	|- ( ( A = _V /\ B = _V ) -> ( A i^i B ) = ( _V i^i _V ) )
2		inv1	|- ( _V i^i _V ) = _V
3	1 2	eqtrdi	|- ( ( A = _V /\ B = _V ) -> ( A i^i B ) = _V )
4		inss1	|- ( A i^i B ) C_ A
5		sseq1	|- ( ( A i^i B ) = _V -> ( ( A i^i B ) C_ A <-> _V C_ A ) )
6	4 5	mpbii	|- ( ( A i^i B ) = _V -> _V C_ A )
7		vss	|- ( _V C_ A <-> A = _V )
8	6 7	sylib	|- ( ( A i^i B ) = _V -> A = _V )
9		inss2	|- ( A i^i B ) C_ B
10		sseq1	|- ( ( A i^i B ) = _V -> ( ( A i^i B ) C_ B <-> _V C_ B ) )
11	9 10	mpbii	|- ( ( A i^i B ) = _V -> _V C_ B )
12		vss	|- ( _V C_ B <-> B = _V )
13	11 12	sylib	|- ( ( A i^i B ) = _V -> B = _V )
14	8 13	jca	|- ( ( A i^i B ) = _V -> ( A = _V /\ B = _V ) )
15	3 14	impbii	|- ( ( A = _V /\ B = _V ) <-> ( A i^i B ) = _V )