Theorem bj-prfromadj

Description: Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-prfromadj	⊢ { 𝑥 , 𝑦 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
2		bj-snfromadj	⊢ { 𝑥 } ∈ V
3		bj-adjg1	⊢ ( { 𝑥 } ∈ V → ( { 𝑥 } ∪ { 𝑦 } ) ∈ V )
4	2 3	ax-mp	⊢ ( { 𝑥 } ∪ { 𝑦 } ) ∈ V
5	1 4	eqeltri	⊢ { 𝑥 , 𝑦 } ∈ V