Metamath Proof Explorer

Theorem rabsstp

Description: Conditions for a restricted class abstraction to be a subset of an unordered triplet. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Assertion rabsstp ⊢ x ∈ V | φ ⊆ X Y Z ↔ ∀ x ∈ V φ → x = X ∨ x = Y ∨ x = Z

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ V | φ = x | x ∈ V ∧ φ
2 dftp2 ⊢ X Y Z = x | x = X ∨ x = Y ∨ x = Z
3 1 2 sseq12i ⊢ x ∈ V | φ ⊆ X Y Z ↔ x | x ∈ V ∧ φ ⊆ x | x = X ∨ x = Y ∨ x = Z
4 ss2ab ⊢ x | x ∈ V ∧ φ ⊆ x | x = X ∨ x = Y ∨ x = Z ↔ ∀ x x ∈ V ∧ φ → x = X ∨ x = Y ∨ x = Z
5 impexp ⊢ x ∈ V ∧ φ → x = X ∨ x = Y ∨ x = Z ↔ x ∈ V → φ → x = X ∨ x = Y ∨ x = Z
6 5 albii ⊢ ∀ x x ∈ V ∧ φ → x = X ∨ x = Y ∨ x = Z ↔ ∀ x x ∈ V → φ → x = X ∨ x = Y ∨ x = Z
7 df-ral ⊢ ∀ x ∈ V φ → x = X ∨ x = Y ∨ x = Z ↔ ∀ x x ∈ V → φ → x = X ∨ x = Y ∨ x = Z
8 6 7 bitr4i ⊢ ∀ x x ∈ V ∧ φ → x = X ∨ x = Y ∨ x = Z ↔ ∀ x ∈ V φ → x = X ∨ x = Y ∨ x = Z
9 3 4 8 3bitri ⊢ x ∈ V | φ ⊆ X Y Z ↔ ∀ x ∈ V φ → x = X ∨ x = Y ∨ x = Z