Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralsn | Structured version Visualization version GIF version |
Description: Convert a quantification over 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 4165 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 df-sbc 3403 df-sn 4126 |
This theorem is referenced by: elixpsn 7833 frfi 8090 dffi3 8220 fseqenlem1 8730 fpwwe2lem13 9343 hashbc 13094 hashf1lem1 13096 eqs1 13245 cshw1 13419 rpnnen2lem11 14792 drsdirfi 16761 0subg 17442 efgsp1 17973 dprd2da 18264 lbsextlem4 18982 ply1coe 19487 mat0dimcrng 20095 txkgen 21265 xkoinjcn 21300 isufil2 21522 ust0 21833 prdsxmetlem 21983 prdsbl 22106 finiunmbl 23119 xrlimcnp 24495 chtub 24737 2sqlem10 24953 dchrisum0flb 24999 pntpbnd1 25075 usgra1v 25919 constr1trl 26118 clwwlkel 26321 rusgranumwlkl1 26474 h1deoi 27792 bnj149 30199 subfacp1lem5 30420 cvmlift2lem1 30538 cvmlift2lem12 30550 lindsenlbs 32574 poimirlem28 32607 poimirlem32 32611 heibor1lem 32778 usgr1e 40471 nbgr2vtx1edg 40572 nbuhgr2vtx1edgb 40574 1wlkl1loop 40842 crctcsh1wlkn0lem7 41019 2pthdlem1 41137 rusgrnumwwlkl1 41172 clwwlksn2 41217 clwwlksel 41221 11wlkdlem4 41307 |
Copyright terms: Public domain | W3C validator |