This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem breng

Description: Equinumerosity relation. This variation of bren does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998) Extract from a subproof of bren . (Revised by BTernaryTau, 23-Sep-2024)

		Ref	Expression
	Assertion	breng	$⊢ (A \in V \land B \in W) \to (A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		f1oeq2	$⊢ x = A \to (f : x \underset{1-1 onto}{⟶} y \leftrightarrow f : A \underset{1-1 onto}{⟶} y)$
2	1	exbidv	$⊢ x = A \to (\exists f f : x \underset{1-1 onto}{⟶} y \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} y)$
3		f1oeq3	$⊢ y = B \to (f : A \underset{1-1 onto}{⟶} y \leftrightarrow f : A \underset{1-1 onto}{⟶} B)$
4	3	exbidv	$⊢ y = B \to (\exists f f : A \underset{1-1 onto}{⟶} y \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$
5		df-en	$⊢ \approx = \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\}$
6	2 4 5	brabg	$⊢ (A \in V \land B \in W) \to (A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$