Metamath Proof Explorer

Theorem elprg

Description: A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of TakeutiZaring p. 15, generalized. (Contributed by NM, 13-Sep-1995)

Ref Expression
Assertion elprg ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ x = y → x = B ↔ y = B
2 eqeq1 ⊢ x = y → x = C ↔ y = C
3 1 2 orbi12d ⊢ x = y → x = B ∨ x = C ↔ y = B ∨ y = C
4 eqeq1 ⊢ y = A → y = B ↔ A = B
5 eqeq1 ⊢ y = A → y = C ↔ A = C
6 4 5 orbi12d ⊢ y = A → y = B ∨ y = C ↔ A = B ∨ A = C
7 dfpr2 ⊢ B C = x | x = B ∨ x = C
8 3 6 7 elab2gw ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C