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