Description: Alternate proof of bj-ideqg from brabga instead of bj-opelid itself proved from bj-opelidb . (Contributed by BJ, 27-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ideqgALT | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reli | ⊢ Rel I | |
| 2 | 1 | brrelex12i | ⊢ ( 𝐴 I 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 3 | 2 | adantl | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 I 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 4 | bj-inexeqex | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) | |
| 5 | eqeq12 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) ) | |
| 6 | df-id | ⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } | |
| 7 | 5 6 | brabga | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) ) |
| 8 | 3 4 7 | pm5.21nd | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) ) |