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	$$⊢\left(A=\mathrm{V}\wedge B=\mathrm{V}\right)\leftrightarrow A\cap B=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ineq12	$$⊢\left(A=\mathrm{V}\wedge B=\mathrm{V}\right)\to A\cap B=\mathrm{V}\cap \mathrm{V}$$
2		inv1	$$⊢\mathrm{V}\cap \mathrm{V}=\mathrm{V}$$
3	1 2	eqtrdi	$$⊢\left(A=\mathrm{V}\wedge B=\mathrm{V}\right)\to A\cap B=\mathrm{V}$$
4		inss1	$$⊢A\cap B\subseteq A$$
5		sseq1	$$⊢A\cap B=\mathrm{V}\to \left(A\cap B\subseteq A\leftrightarrow \mathrm{V}\subseteq A\right)$$
6	4 5	mpbii	$$⊢A\cap B=\mathrm{V}\to \mathrm{V}\subseteq A$$
7		vss	$$⊢\mathrm{V}\subseteq A\leftrightarrow A=\mathrm{V}$$
8	6 7	sylib	$$⊢A\cap B=\mathrm{V}\to A=\mathrm{V}$$
9		inss2	$$⊢A\cap B\subseteq B$$
10		sseq1	$$⊢A\cap B=\mathrm{V}\to \left(A\cap B\subseteq B\leftrightarrow \mathrm{V}\subseteq B\right)$$
11	9 10	mpbii	$$⊢A\cap B=\mathrm{V}\to \mathrm{V}\subseteq B$$
12		vss	$$⊢\mathrm{V}\subseteq B\leftrightarrow B=\mathrm{V}$$
13	11 12	sylib	$$⊢A\cap B=\mathrm{V}\to B=\mathrm{V}$$
14	8 13	jca	$$⊢A\cap B=\mathrm{V}\to \left(A=\mathrm{V}\wedge B=\mathrm{V}\right)$$
15	3 14	impbii	$$⊢\left(A=\mathrm{V}\wedge B=\mathrm{V}\right)\leftrightarrow A\cap B=\mathrm{V}$$