# 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}\in {V}\to \left({A}\in \left\{{B},{C}\right\}↔\left({A}={B}\vee {A}={C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqeq1 ${⊢}{x}={y}\to \left({x}={B}↔{y}={B}\right)$
2 eqeq1 ${⊢}{x}={y}\to \left({x}={C}↔{y}={C}\right)$
3 1 2 orbi12d ${⊢}{x}={y}\to \left(\left({x}={B}\vee {x}={C}\right)↔\left({y}={B}\vee {y}={C}\right)\right)$
4 eqeq1 ${⊢}{y}={A}\to \left({y}={B}↔{A}={B}\right)$
5 eqeq1 ${⊢}{y}={A}\to \left({y}={C}↔{A}={C}\right)$
6 4 5 orbi12d ${⊢}{y}={A}\to \left(\left({y}={B}\vee {y}={C}\right)↔\left({A}={B}\vee {A}={C}\right)\right)$
7 dfpr2 ${⊢}\left\{{B},{C}\right\}=\left\{{x}|\left({x}={B}\vee {x}={C}\right)\right\}$
8 3 6 7 elab2gw ${⊢}{A}\in {V}\to \left({A}\in \left\{{B},{C}\right\}↔\left({A}={B}\vee {A}={C}\right)\right)$