Theorem bj-prex

Description: Existence of unordered pairs proved from ax-bj-sn and ax-bj-bun . (Contributed by BJ, 12-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-prex	|- { A , B } e. _V

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		bj-snex	|- { A } e. _V
3		bj-snex	|- { B } e. _V
4		bj-unexg	|- ( ( { A } e. _V /\ { B } e. _V ) -> ( { A } u. { B } ) e. _V )
5	2 3 4	mp2an	|- ( { A } u. { B } ) e. _V
6	1 5	eqeltri	|- { A , B } e. _V