![]() |
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 2130, ax-12 2167. (Revised by GG, 30-Sep-2024.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexsng | ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsng.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | notbid 317 | . . 3 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | 2 | ralsng 4672 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓)) |
4 | dfrex2 3063 | . . 3 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑) | |
5 | bicom1 220 | . . . 4 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑)) | |
6 | 5 | con1bid 354 | . . 3 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ 𝜓)) |
7 | 4, 6 | bitrid 282 | . 2 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
8 | 3, 7 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ∃wrex 3060 {csn 4623 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-v 3464 df-sn 4624 |
This theorem is referenced by: rexsn 4681 rextpg 4698 iunxsng 5090 frirr 5651 frsn 5761 imasng 6085 naddunif 8715 scshwfzeqfzo 14830 dvdsprmpweqnn 16882 mnd1 18764 grp1 19037 pzriprnglem3 21469 pzriprnglem10 21476 psdmul 22156 elntg2 28916 1loopgrvd0 29438 1egrvtxdg0 29445 nfrgr2v 30202 1vwmgr 30206 elgrplsmsn 33271 grplsmid 33285 ballotlemfc0 34339 ballotlemfcc 34340 bj-restsn 36802 elrnressn 37984 elpaddat 39516 elpadd2at 39518 brfvidRP 43392 mnuunid 43988 iccelpart 47041 zlidlring 47647 lco0 47846 |
Copyright terms: Public domain | W3C validator |