Theorem bj-abv

Description: The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-abv	$$⊢\forall x\phi \to \left\{x|\phi \right\}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		trud	$$⊢\left(\phi \wedge \phi \right)\to \top$$
2		simpl	$$⊢\left(\phi \wedge \top \right)\to \phi$$
3	1 2	impbida	$$⊢\phi \to \left(\phi \leftrightarrow \top \right)$$
4	3	alimi	$$⊢\forall x\phi \to \forall x\left(\phi \leftrightarrow \top \right)$$
5		abbi	$$⊢\forall x\left(\phi \leftrightarrow \top \right)\to \left\{x|\phi \right\}=\left\{x|\top \right\}$$
6	4 5	syl	$$⊢\forall x\phi \to \left\{x|\phi \right\}=\left\{x|\top \right\}$$
7		dfv2	$$⊢\mathrm{V}=\left\{x|\top \right\}$$
8	6 7	eqtr4di	$$⊢\forall x\phi \to \left\{x|\phi \right\}=\mathrm{V}$$