| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralsn | Structured version Visualization version GIF version | ||
| Description: Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
| Ref | Expression |
|---|---|
| ralsn.1 | ⊢ 𝐴 ∈ V |
| ralsn.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| ralsn | ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralsn.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | ralsn.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | ralsng 4675 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-sn 4627 |
| This theorem is referenced by: xpord2indlem 8172 xpord3inddlem 8179 naddcllem 8714 naddasslem1 8732 naddasslem2 8733 elixpsn 8977 frfi 9321 dffi3 9471 ssttrcl 9755 ttrclss 9760 ttrclselem2 9766 fseqenlem1 10064 fpwwe2lem12 10682 hashbc 14492 hashf1lem1 14494 eqs1 14650 cshw1 14860 rpnnen2lem11 16260 drsdirfi 18351 0subg 19169 0subgOLD 19170 0subgALT 19586 efgsp1 19755 dprd2da 20062 lbsextlem4 21163 rnglidl0 21239 ply1coe 22302 mat0dimcrng 22476 txkgen 23660 xkoinjcn 23695 isufil2 23916 ust0 24228 prdsxmetlem 24378 prdsbl 24504 finiunmbl 25579 xrlimcnp 27011 chtub 27256 2sqlem10 27472 dchrisum0flb 27554 pntpbnd1 27630 conway 27844 etasslt 27858 slerec 27864 bday1s 27876 madebdaylemlrcut 27937 precsexlem9 28239 zscut 28393 nohalf 28407 halfcut 28416 addhalfcut 28419 usgr1e 29262 nbgr2vtx1edg 29367 nbuhgr2vtx1edgb 29369 wlkl1loop 29656 crctcshwlkn0lem7 29836 2pthdlem1 29950 rusgrnumwwlkl1 29988 clwwlkccatlem 30008 clwwlkn2 30063 clwwlkel 30065 clwwlkwwlksb 30073 1wlkdlem4 30159 h1deoi 31568 bnj149 34889 subfacp1lem5 35189 cvmlift2lem1 35307 cvmlift2lem12 35319 lindsenlbs 37622 poimirlem28 37655 poimirlem32 37659 heibor1lem 37816 nadd1suc 43405 usgrexmpl1lem 47980 usgrexmpl2lem 47985 |
| Copyright terms: Public domain | W3C validator |