Theorem elprg 4585

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 2744	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		eqeq1 2744	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶))
3	1, 2	orbi12d 924	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
4		dfpr2 4583	. 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
5	3, 4	elab2g 3625	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 853   = wceq 1547   ∈ wcel 2119  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  elpri  4586  elpr  4587  elpr2g  4588  nelpr2  4592  nelpr1  4593  eldifpr  4597  eltpg  4625  ifpr  4632  prid1g  4699  ssprss  4762  preq1b  4784  prel12g  4802  ordunpr  7773  hashtpg  14445  2nsgsimpgd  20077  cnsubrg  21409  atandm  26865  1egrvtxdg0  29605  eupth2lem1  30313  nelpr  32626  eliccioo  33016  linds2eq  33471  sfprmdvdsmersenne  48088  prelrrx2b  49212