![]() |
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 2138, ax-12 2172. (Revised by Gino Giotto, 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 4639 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓)) |
4 | dfrex2 3077 | . . 3 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ ¬ ∀𝑥 ∈ {𝐴} ¬ 𝜑) | |
5 | bicom1 220 | . . . 4 ⊢ ((∀𝑥 ∈ {𝐴} ¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜓 ↔ ∀𝑥 ∈ {𝐴} ¬ 𝜑)) | |
6 | 5 | con1bid 356 | . . 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 205 = wceq 1542 ∈ wcel 2107 ∀wral 3065 ∃wrex 3074 {csn 4591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-v 3450 df-sn 4592 |
This theorem is referenced by: rexsn 4648 rextpg 4665 iunxsng 5055 frirr 5615 frsn 5724 imasng 6040 naddunif 8644 scshwfzeqfzo 14722 dvdsprmpweqnn 16764 mnd1 18604 grp1 18861 elntg2 27976 1loopgrvd0 28494 1egrvtxdg0 28501 nfrgr2v 29258 1vwmgr 29262 elgrplsmsn 32211 grplsmid 32225 ballotlemfc0 33132 ballotlemfcc 33133 bj-restsn 35582 elrnressn 36762 elpaddat 38296 elpadd2at 38298 brfvidRP 42034 mnuunid 42631 iccelpart 45699 zlidlring 46300 lco0 46582 |
Copyright terms: Public domain | W3C validator |