Theorem opabid2ss

Description: One direction of opabid2 which holds without a Rel A requirement. (Contributed by Thierry Arnoux, 18-Feb-2022)

	Ref	Expression
Assertion	opabid2ss	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
2	1	opabssi	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ⊆ 𝐴