Theorem bj-prexg

Description: Existence of unordered pairs formed on sets, proved from ax-bj-sn and ax-bj-bun . Contrary to bj-prex , this proof is intuitionistically valid and does not require ax-nul . (Contributed by BJ, 12-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-prexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 , 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		bj-snexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ V )
3		bj-snexg	⊢ ( 𝐵 ∈ 𝑊 → { 𝐵 } ∈ V )
4		bj-unexg	⊢ ( ( { 𝐴 } ∈ V ∧ { 𝐵 } ∈ V ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ V )
5	2 3 4	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ V )
6	1 5	eqeltrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 , 𝐵 } ∈ V )