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	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		reli	⊢ Rel I
2	1	brrelex12i	⊢ ( 𝐴 I 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3	2	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) ∧ 𝐴 I 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
5	4	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ V )
6		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
7	6	biimparc	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑊 )
8	7	elexd	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ V )
9	5 8	jaoian	⊢ ( ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ V )
10		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
11	10	biimpac	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑉 )
12	11	elexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
13		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
14	13	adantr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
15	12 14	jaoian	⊢ ( ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
16	9 15	jca	⊢ ( ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
17		eqeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
18		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
19	17 18	brabga	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )
20	3 16 19	pm5.21nd	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )