![]() |
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 2741 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | eqeq1 2741 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
3 | 1, 2 | orbi12d 917 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
4 | dfpr2 4603 | . 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
5 | 3, 4 | elab2g 3630 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 845 = wceq 1541 ∈ wcel 2106 {cpr 4586 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-un 3913 df-sn 4585 df-pr 4587 |
This theorem is referenced by: elpri 4606 elpr 4607 elpr2g 4608 elpr2OLD 4610 nelpr2 4611 nelpr1 4612 eldifpr 4616 eltpg 4644 ifpr 4650 prid1g 4719 ssprss 4782 preq1b 4802 prel12g 4819 ordunpr 7753 hashtpg 14338 2nsgsimpgd 19840 cnsubrg 20810 atandm 26178 1egrvtxdg0 28288 eupth2lem1 28991 nelpr 31287 eliccioo 31613 linds2eq 31994 sfprmdvdsmersenne 45696 prelrrx2b 46701 |
Copyright terms: Public domain | W3C validator |