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 1915 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ralsng.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | ralsngf 4611 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1537 ∈ wcel 2114 ∀wral 3138 {csn 4567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 df-sbc 3773 df-sn 4568 |
This theorem is referenced by: 2ralsng 4616 ralsn 4619 raltpg 4634 ralunsn 4824 iinxsng 5010 frirr 5532 posn 5637 frsn 5639 f12dfv 7030 ranksnb 9256 mgm1 17868 sgrp1 17910 mnd1 17952 grp1 18206 cntzsnval 18454 abl1 18986 srgbinomlem4 19293 ring1 19352 mat1dimmul 21085 ufileu 22527 istrkg3ld 26247 1hevtxdg0 27287 wlkp1lem8 27462 wwlksnext 27671 wwlksext2clwwlk 27836 dfconngr1 27967 1conngr 27973 frgr1v 28050 lindssn 30939 lbslsat 31014 bj-raldifsn 34395 lindsadd 34900 poimirlem26 34933 poimirlem27 34934 poimirlem31 34938 zlidlring 44219 linds0 44540 snlindsntor 44546 lmod1 44567 |
Copyright terms: Public domain | W3C validator |