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 4605 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 ∀wral 3135 Vcvv 3492 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-v 3494 df-sbc 3770 df-sn 4558 |
This theorem is referenced by: elixpsn 8489 frfi 8751 dffi3 8883 fseqenlem1 9438 fpwwe2lem13 10052 hashbc 13799 hashf1lem1 13801 eqs1 13954 cshw1 14172 rpnnen2lem11 15565 drsdirfi 17536 0subg 18242 efgsp1 18792 dprd2da 19093 lbsextlem4 19862 ply1coe 20392 mat0dimcrng 21007 txkgen 22188 xkoinjcn 22223 isufil2 22444 ust0 22755 prdsxmetlem 22905 prdsbl 23028 finiunmbl 24072 xrlimcnp 25473 chtub 25715 2sqlem10 25931 dchrisum0flb 26013 pntpbnd1 26089 usgr1e 26954 nbgr2vtx1edg 27059 nbuhgr2vtx1edgb 27061 wlkl1loop 27346 crctcshwlkn0lem7 27521 2pthdlem1 27636 rusgrnumwwlkl1 27674 clwwlkccatlem 27694 clwwlkn2 27749 clwwlkel 27752 clwwlkwwlksb 27760 1wlkdlem4 27846 h1deoi 29253 bnj149 32046 subfacp1lem5 32328 cvmlift2lem1 32446 cvmlift2lem12 32458 conway 33161 etasslt 33171 slerec 33174 lindsenlbs 34768 poimirlem28 34801 poimirlem32 34805 heibor1lem 34968 |
Copyright terms: Public domain | W3C validator |