|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > rexsng | Structured version Visualization version GIF version | ||
| Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2140, ax-12 2176. (Revised by GG, 30-Sep-2024.) | 
| Ref | Expression | 
|---|---|
| ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| rexsng | ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ralsng.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | notbid 318 | . . 3 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓)) | 
| 3 | 2 | ralsng 4674 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓)) | 
| 4 | dfrex2 3072 | . . 3 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑) | |
| 5 | bicom1 221 | . . . 4 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑)) | |
| 6 | 5 | con1bid 355 | . . 3 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ 𝜓)) | 
| 7 | 4, 6 | bitrid 283 | . 2 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | 
| 8 | 3, 7 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1539 ∈ wcel 2107 ∀wral 3060 ∃wrex 3069 {csn 4625 | 
| 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-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-v 3481 df-sn 4626 | 
| This theorem is referenced by: rexsn 4681 rextpg 4698 iunxsng 5089 frirr 5660 frsn 5772 imasng 6101 naddunif 8732 scshwfzeqfzo 14866 dvdsprmpweqnn 16924 mnd1 18793 grp1 19066 pzriprnglem3 21495 pzriprnglem10 21502 psdmul 22171 cutmax 27969 cutmin 27970 halfcut 28417 elntg2 29001 1loopgrvd0 29523 1egrvtxdg0 29530 nfrgr2v 30292 1vwmgr 30296 elgrplsmsn 33419 grplsmid 33433 ballotlemfc0 34496 ballotlemfcc 34497 bj-restsn 37084 elrnressn 38275 elpaddat 39807 elpadd2at 39809 brfvidRP 43706 mnuunid 44301 iccelpart 47425 zlidlring 48155 lco0 48349 | 
| Copyright terms: Public domain | W3C validator |