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	⊢ ( ( 𝐴 = V ∧ 𝐵 = V ) ↔ ( 𝐴 ∩ 𝐵 ) = V )

Proof

Step	Hyp	Ref	Expression
1		ineq12	⊢ ( ( 𝐴 = V ∧ 𝐵 = V ) → ( 𝐴 ∩ 𝐵 ) = ( V ∩ V ) )
2		inv1	⊢ ( V ∩ V ) = V
3	1 2	eqtrdi	⊢ ( ( 𝐴 = V ∧ 𝐵 = V ) → ( 𝐴 ∩ 𝐵 ) = V )
4		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
5		sseq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ V ⊆ 𝐴 ) )
6	4 5	mpbii	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → V ⊆ 𝐴 )
7		vss	⊢ ( V ⊆ 𝐴 ↔ 𝐴 = V )
8	6 7	sylib	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → 𝐴 = V )
9		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
10		sseq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ↔ V ⊆ 𝐵 ) )
11	9 10	mpbii	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → V ⊆ 𝐵 )
12		vss	⊢ ( V ⊆ 𝐵 ↔ 𝐵 = V )
13	11 12	sylib	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → 𝐵 = V )
14	8 13	jca	⊢ ( ( 𝐴 ∩ 𝐵 ) = V → ( 𝐴 = V ∧ 𝐵 = V ) )
15	3 14	impbii	⊢ ( ( 𝐴 = V ∧ 𝐵 = V ) ↔ ( 𝐴 ∩ 𝐵 ) = V )