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	|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		bj-snexg	|- ( A e. V -> { A } e. _V )
3		bj-snexg	|- ( B e. W -> { B } e. _V )
4		bj-unexg	|- ( ( { A } e. _V /\ { B } e. _V ) -> ( { A } u. { B } ) e. _V )
5	2 3 4	syl2an	|- ( ( A e. V /\ B e. W ) -> ( { A } u. { B } ) e. _V )
6	1 5	eqeltrid	|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )