![]() |
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 4673 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 ∀wral 3056 Vcvv 3469 {csn 4624 |
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 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 df-v 3471 df-sn 4625 |
This theorem is referenced by: xpord2indlem 8146 xpord3inddlem 8153 naddcllem 8690 naddasslem1 8708 naddasslem2 8709 elixpsn 8949 frfi 9306 dffi3 9448 ssttrcl 9732 ttrclss 9737 ttrclselem2 9743 fseqenlem1 10041 fpwwe2lem12 10659 hashbc 14438 hashf1lem1 14441 hashf1lem1OLD 14442 eqs1 14588 cshw1 14798 rpnnen2lem11 16194 drsdirfi 18290 0subg 19099 0subgOLD 19100 0subgALT 19516 efgsp1 19685 dprd2da 19992 lbsextlem4 21042 rnglidl0 21118 ply1coe 22210 mat0dimcrng 22365 txkgen 23549 xkoinjcn 23584 isufil2 23805 ust0 24117 prdsxmetlem 24267 prdsbl 24393 finiunmbl 25466 xrlimcnp 26893 chtub 27138 2sqlem10 27354 dchrisum0flb 27436 pntpbnd1 27512 conway 27725 etasslt 27739 slerec 27745 bday1s 27757 madebdaylemlrcut 27818 precsexlem9 28106 usgr1e 29051 nbgr2vtx1edg 29156 nbuhgr2vtx1edgb 29158 wlkl1loop 29445 crctcshwlkn0lem7 29620 2pthdlem1 29734 rusgrnumwwlkl1 29772 clwwlkccatlem 29792 clwwlkn2 29847 clwwlkel 29849 clwwlkwwlksb 29857 1wlkdlem4 29943 h1deoi 31352 bnj149 34496 subfacp1lem5 34784 cvmlift2lem1 34902 cvmlift2lem12 34914 lindsenlbs 37077 poimirlem28 37110 poimirlem32 37114 heibor1lem 37271 nadd1suc 42793 |
Copyright terms: Public domain | W3C validator |