abv

Description: The class of sets verifying a property is the universal class if and only if that property is a tautology. The reverse implication ( bj-abv ) requires fewer axioms. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by GG, 30-Aug-2024) (Proof shortened by BJ, 30-Aug-2024)

		Ref	Expression
	Assertion	abv	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
2		vextru	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
3	2	tbt	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
5	3 4	bitr3i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6	5	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
7	1 6	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
8		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
9	8	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } )
10		sb8v	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
11	7 9 10	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 )

Metamath Proof Explorer

Theorem abv

Proof