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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		f1oeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –1-1-onto→ 𝑦 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝑦 ) )
2	1	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑦 ) )
3		f1oeq3	⊢ ( 𝑦 = 𝐵 → ( 𝑓 : 𝐴 –1-1-onto→ 𝑦 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
4	3	exbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
5		df-en	⊢ ≈ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑦 }
6	2 4 5	brabg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )