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.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralsng | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsnsg 4163 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
2 | ralsng.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbcieg 3435 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
4 | 1, 3 | bitrd 267 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 ∀wral 2896 [wsbc 3402 {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: 2ralsng 4167 ralsn 4169 ralprg 4181 raltpg 4183 ralunsn 4360 iinxsng 4536 frirr 5015 posn 5110 frsn 5112 f12dfv 6429 ranksnb 8573 mgm1 17080 sgrp1 17116 mnd1 17154 grp1 17345 cntzsnval 17580 abl1 18092 srgbinomlem4 18366 ring1 18425 mat1dimmul 20101 ufileu 21533 istrkg3ld 25160 cusgra1v 25990 cusgra2v 25991 dfconngra1 26199 1conngra 26203 wwlknext 26252 clwwlkn2 26303 wwlkext2clwwlk 26331 rusgrasn 26472 frgra1v 26525 poimirlem26 32605 poimirlem27 32606 poimirlem31 32610 1hevtxdg0 40720 1wlkp1lem8 40889 wwlksnext 41099 wwlksext2clwwlk 41231 dfconngr1 41355 1conngr 41361 frgr1v 41441 zlidlring 41718 linds0 42048 snlindsntor 42054 lmod1 42075 |
Copyright terms: Public domain | W3C validator |