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	⊢ ( ∀ 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = V )

Proof

Step	Hyp	Ref	Expression
1		trud	⊢ ( ( 𝜑 ∧ 𝜑 ) → ⊤ )
2		simpl	⊢ ( ( 𝜑 ∧ ⊤ ) → 𝜑 )
3	1 2	impbida	⊢ ( 𝜑 → ( 𝜑 ↔ ⊤ ) )
4	3	alimi	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜑 ↔ ⊤ ) )
5		abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ ⊤ ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } )
6	4 5	syl	⊢ ( ∀ 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } )
7		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
8	6 7	eqtr4di	⊢ ( ∀ 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = V )