Metamath Proof Explorer

Theorem bj-ideqg1ALT

Description: Alternate proof of bj-ideqg1 using brabga instead of the "unbounded" version bj-brab2a1 or brab2a . (Contributed by BJ, 25-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

TODO: delete once bj-ideqg is in the main section.

Ref Expression
Assertion bj-ideqg1ALT ⊢ A ∈ V ∨ B ∈ W → A I B ↔ A = B

Proof

Step Hyp Ref Expression
1 reli ⊢ Rel ⁡ I
2 1 brrelex12i ⊢ A I B → A ∈ V ∧ B ∈ V
3 2 adantl ⊢ A ∈ V ∨ B ∈ W ∧ A I B → A ∈ V ∧ B ∈ V
4 elex ⊢ A ∈ V → A ∈ V
5 4 adantr ⊢ A ∈ V ∧ A = B → A ∈ V
6 eleq1 ⊢ A = B → A ∈ W ↔ B ∈ W
7 6 biimparc ⊢ B ∈ W ∧ A = B → A ∈ W
8 7 elexd ⊢ B ∈ W ∧ A = B → A ∈ V
9 5 8 jaoian ⊢ A ∈ V ∨ B ∈ W ∧ A = B → A ∈ V
10 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
11 10 biimpac ⊢ A ∈ V ∧ A = B → B ∈ V
12 11 elexd ⊢ A ∈ V ∧ A = B → B ∈ V
13 elex ⊢ B ∈ W → B ∈ V
14 13 adantr ⊢ B ∈ W ∧ A = B → B ∈ V
15 12 14 jaoian ⊢ A ∈ V ∨ B ∈ W ∧ A = B → B ∈ V
16 9 15 jca ⊢ A ∈ V ∨ B ∈ W ∧ A = B → A ∈ V ∧ B ∈ V
17 eqeq12 ⊢ x = A ∧ y = B → x = y ↔ A = B
18 df-id ⊢ I = x y | x = y
19 17 18 brabga ⊢ A ∈ V ∧ B ∈ V → A I B ↔ A = B
20 3 16 19 pm5.21nd ⊢ A ∈ V ∨ B ∈ W → A I B ↔ A = B