|   | 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 2740 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
| 2 | eqeq1 2740 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
| 3 | 1, 2 | orbi12d 918 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | 
| 4 | dfpr2 4645 | . 2 ⊢ {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | |
| 5 | 3, 4 | elab2g 3679 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1539 ∈ wcel 2107 {cpr 4627 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-sn 4626 df-pr 4628 | 
| This theorem is referenced by: elpri 4648 elpr 4649 elpr2g 4650 nelpr2 4652 nelpr1 4653 eldifpr 4657 eltpg 4685 ifpr 4692 prid1g 4759 ssprss 4823 preq1b 4845 prel12g 4863 ordunpr 7847 hashtpg 14525 2nsgsimpgd 20123 cnsubrg 21446 atandm 26920 1egrvtxdg0 29530 eupth2lem1 30238 nelpr 32550 eliccioo 32914 linds2eq 33410 sfprmdvdsmersenne 47595 prelrrx2b 48640 | 
| Copyright terms: Public domain | W3C validator |