Theorem breng

Description: Equinumerosity relation. This variation of bren does not require the Axiom of Union. (Contributed by BTernaryTau, 23-Sep-2024)

	Ref	Expression
Assertion	breng	|- ( ( A e. V /\ B e. W ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )

Proof

Step	Hyp	Ref	Expression
1		f1oeq2	|- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
2	1	exbidv	|- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
3		f1oeq3	|- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
4	3	exbidv	|- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
5		df-en	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
6	2 4 5	brabg	|- ( ( A e. V /\ B e. W ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )