Theorem elprg 4546

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 variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2802	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐵 ↔ 𝑦 = 𝐵))
2		eqeq1 2802	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐶 ↔ 𝑦 = 𝐶))
3	1, 2	orbi12d 916	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑦 = 𝐵 ∨ 𝑦 = 𝐶)))
4		eqeq1 2802	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 = 𝐵 ↔ 𝐴 = 𝐵))
5		eqeq1 2802	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 = 𝐶 ↔ 𝐴 = 𝐶))
6	4, 5	orbi12d 916	. 2 ⊢ (𝑦 = 𝐴 → ((𝑦 = 𝐵 ∨ 𝑦 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
7		dfpr2 4544	. 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
8	3, 6, 7	elab2gw 3613	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  elpri  4547  elpr  4548  elpr2g  4549  elpr2OLD  4551  nelpr2  4552  nelpr1  4553  eldifpr  4557  eltpg  4583  ifpr  4589  prid1g  4656  ssprss  4717  preq1b  4737  prel12g  4754  ordunpr  7521  hashtpg  13839  2nsgsimpgd  19217  cnsubrg  20151  atandm  25462  1egrvtxdg0  27301  eupth2lem1  28003  nelpr  30303  eliccioo  30633  linds2eq  30995  sfprmdvdsmersenne  44121  prelrrx2b  45128