Metamath Proof Explorer

Theorem elprg

Description: A member of an unordered pair of classes is one or the other of them. 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 = A → x = B ↔ A = B
2 eqeq1 ⊢ x = A → x = C ↔ A = C
3 1 2 orbi12d ⊢ x = A → x = B ∨ x = C ↔ A = B ∨ A = C
4 dfpr2 ⊢ B C = x | x = B ∨ x = C
5 3 4 elab2g ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C