Theorem elprg 4613

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.)

Assertion

Ref	Expression
elprg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))

Proof of Theorem elprg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2767	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		eqeq1 2767	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶))
3	1, 2	orbi12d 931	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
4		dfpr2 4611	. 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
5	3, 4	elab2g 3640	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860   = wceq 1570   ∈ wcel 2143  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  elpri  4614  elpr  4615  elpr2g  4616  nelpr2  4620  nelpr1  4621  eldifpr  4625  eltpg  4653  ifpr  4660  prid1g  4727  ssprss  4791  preq1b  4812  prel12g  4830  ordunpr  7823  hashtpg  14524  2nsgsimpgd  20175  cnsubrg  21558  atandm  27019  1egrvtxdg0  29839  eupth2lem1  30547  nelpr  32855  eliccioo  33228  linds2eq  33672  sfprmdvdsmersenne  48332  prelrrx2b  49471