Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralsng | Structured version Visualization version GIF version |
Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralsng | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1906 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ralsng.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | ralsngf 4603 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 ∀wral 3135 {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: 2ralsng 4608 ralsn 4611 raltpg 4626 ralunsn 4816 iinxsng 5001 frirr 5525 posn 5630 frsn 5632 f12dfv 7021 ranksnb 9244 mgm1 17856 sgrp1 17898 mnd1 17940 grp1 18144 cntzsnval 18392 abl1 18915 srgbinomlem4 19222 ring1 19281 mat1dimmul 21013 ufileu 22455 istrkg3ld 26174 1hevtxdg0 27214 wlkp1lem8 27389 wwlksnext 27598 wwlksext2clwwlk 27763 dfconngr1 27894 1conngr 27900 frgr1v 27977 lindssn 30866 lbslsat 30913 bj-raldifsn 34286 lindsadd 34766 poimirlem26 34799 poimirlem27 34800 poimirlem31 34804 zlidlring 44127 linds0 44448 snlindsntor 44454 lmod1 44475 |
Copyright terms: Public domain | W3C validator |