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 2742 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | eqeq1 2742 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
3 | 1, 2 | orbi12d 918 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
4 | dfpr2 4535 | . 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
5 | 3, 4 | elab2g 3575 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∨ wo 846 = wceq 1542 ∈ wcel 2114 {cpr 4518 |
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 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3848 df-sn 4517 df-pr 4519 |
This theorem is referenced by: elpri 4538 elpr 4539 elpr2g 4540 elpr2OLD 4542 nelpr2 4543 nelpr1 4544 eldifpr 4548 eltpg 4576 ifpr 4582 prid1g 4651 ssprss 4712 preq1b 4732 prel12g 4749 ordunpr 7560 hashtpg 13937 2nsgsimpgd 19343 cnsubrg 20277 atandm 25614 1egrvtxdg0 27453 eupth2lem1 28155 nelpr 30453 eliccioo 30780 linds2eq 31147 sfprmdvdsmersenne 44589 prelrrx2b 45594 |
Copyright terms: Public domain | W3C validator |