![]() |
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.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralsng | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 3066 | . . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑)) | |
2 | velsn 4607 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
3 | 2 | imbi1i 350 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)) |
4 | 3 | albii 1822 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) |
5 | 1, 4 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) |
6 | elisset 2820 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
7 | ralsng.1 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 7 | pm5.74i 271 | . . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
9 | 8 | albii 1822 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
10 | 9 | a1i 11 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))) |
11 | 19.23v 1946 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
12 | 11 | a1i 11 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
13 | pm5.5 362 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓)) | |
14 | 10, 12, 13 | 3bitrd 305 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
15 | 6, 14 | syl 17 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
16 | 5, 15 | bitrid 283 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3065 {csn 4591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-v 3450 df-sn 4592 |
This theorem is referenced by: rexsng 4640 2ralsng 4642 ralsn 4647 ralprg 4660 raltpg 4664 ralunsn 4856 iinxsng 5053 frirr 5615 posn 5722 frsn 5724 f12dfv 7224 naddov2 8630 naddunif 8644 naddasslem1 8645 naddasslem2 8646 ranksnb 9770 mgm1 18520 sgrp1 18562 mnd1 18604 grp1 18861 cntzsnval 19111 abl1 19651 srgbinomlem4 19967 ring1 20033 mat1dimmul 21841 ufileu 23286 istrkg3ld 27445 1hevtxdg0 28495 wlkp1lem8 28670 wwlksnext 28880 wwlksext2clwwlk 29043 dfconngr1 29174 1conngr 29180 frgr1v 29257 lindssn 32206 lbslsat 32353 bj-raldifsn 35600 lindsadd 36100 poimirlem26 36133 poimirlem27 36134 poimirlem31 36138 cantnfresb 41688 safesnsupfilb 41764 cfsetsnfsetf1 45367 zlidlring 46300 linds0 46620 snlindsntor 46626 lmod1 46647 |
Copyright terms: Public domain | W3C validator |