![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elprg | Structured version Visualization version GIF version |
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 |
---|---|
elprg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2735 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | eqeq1 2735 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
3 | 1, 2 | orbi12d 916 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
4 | dfpr2 4647 | . 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
5 | 3, 4 | elab2g 3670 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 844 = wceq 1540 ∈ wcel 2105 {cpr 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-un 3953 df-sn 4629 df-pr 4631 |
This theorem is referenced by: elpri 4650 elpr 4651 elpr2g 4652 elpr2OLD 4654 nelpr2 4655 nelpr1 4656 eldifpr 4660 eltpg 4689 ifpr 4695 prid1g 4764 ssprss 4827 preq1b 4847 prel12g 4864 ordunpr 7818 hashtpg 14451 2nsgsimpgd 20014 cnsubrg 21206 atandm 26618 1egrvtxdg0 29036 eupth2lem1 29739 nelpr 32036 eliccioo 32365 linds2eq 32772 sfprmdvdsmersenne 46570 prelrrx2b 47488 |
Copyright terms: Public domain | W3C validator |