![]() |
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 4520 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 ∈ wcel 2081 ∀wral 3105 Vcvv 3437 {csn 4472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-v 3439 df-sbc 3707 df-sn 4473 |
This theorem is referenced by: elixpsn 8349 frfi 8609 dffi3 8741 fseqenlem1 9296 fpwwe2lem13 9910 hashbc 13659 hashf1lem1 13661 eqs1 13810 cshw1 14020 rpnnen2lem11 15410 drsdirfi 17377 0subg 18058 efgsp1 18590 dprd2da 18881 lbsextlem4 19623 ply1coe 20147 mat0dimcrng 20763 txkgen 21944 xkoinjcn 21979 isufil2 22200 ust0 22511 prdsxmetlem 22661 prdsbl 22784 finiunmbl 23828 xrlimcnp 25228 chtub 25470 2sqlem10 25686 dchrisum0flb 25768 pntpbnd1 25844 usgr1e 26710 nbgr2vtx1edg 26815 nbuhgr2vtx1edgb 26817 wlkl1loop 27102 crctcshwlkn0lem7 27281 2pthdlem1 27396 rusgrnumwwlkl1 27434 clwwlkccatlem 27454 clwwlkn2 27509 clwwlkel 27512 clwwlkwwlksb 27520 1wlkdlem4 27606 h1deoi 29017 bnj149 31763 subfacp1lem5 32039 cvmlift2lem1 32157 cvmlift2lem12 32169 conway 32873 etasslt 32883 slerec 32886 lindsenlbs 34418 poimirlem28 34451 poimirlem32 34455 heibor1lem 34619 |
Copyright terms: Public domain | W3C validator |