Theorem cvjust

Description: Every set is a class. Proposition 4.9 of TakeutiZaring p. 13. This theorem shows that a setvar variable can be expressed as a class abstraction. This provides a motivation for the class syntax construction cv , which allows us to substitute a setvar variable for a class variable. See also cab and df-clab . Note that this is not a rigorous justification, because cv is used as part of the proof of this theorem, but a careful argument can be made outside of the formalism of Metamath, for example as is done in Chapter 4 of Takeuti and Zaring. See also the discussion under the definition of class in Jech p. 4 showing that "Every set can be considered to be a class." See abid1 for the version of cvjust extended to classes. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Wolf Lammen, 4-May-2023)

	Ref	Expression
Assertion	cvjust	⊢ 𝑥 = { 𝑦 ∣ 𝑦 ∈ 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝑥 = { 𝑦 ∣ 𝑦 ∈ 𝑥 } ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ { 𝑦 ∣ 𝑦 ∈ 𝑥 } ) )
2		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝑦 ∈ 𝑥 } ↔ [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝑥 )
3		elsb1	⊢ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 )
4	2 3	bitr2i	⊢ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ { 𝑦 ∣ 𝑦 ∈ 𝑥 } )
5	1 4	mpgbir	⊢ 𝑥 = { 𝑦 ∣ 𝑦 ∈ 𝑥 }