![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elprg | Structured version Visualization version GIF version |
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elprg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2764 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | eqeq1 2764 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
3 | 1, 2 | orbi12d 748 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
4 | dfpr2 4339 | . 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
5 | 3, 4 | elab2g 3493 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∨ wo 382 = wceq 1632 ∈ wcel 2139 {cpr 4323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-un 3720 df-sn 4322 df-pr 4324 |
This theorem is referenced by: elpri 4342 elpr 4343 elpr2 4344 elpr2OLD 4345 eldifpr 4349 eltpg 4371 ifpr 4377 prid1g 4439 ssprss 4501 preq1b 4522 prel12g 4544 ordunpr 7192 hashtpg 13479 cnsubrg 20028 atandm 24823 1egrvtxdg0 26638 eupth2lem1 27391 eliccioo 29969 nelpr2 39778 nelpr1 39779 sfprmdvdsmersenne 42048 |
Copyright terms: Public domain | W3C validator |