![]() |
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 2139, ax-12 2175. (Revised by GG, 30-Sep-2024.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralsng | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 3060 | . . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑)) | |
2 | velsn 4647 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
3 | 2 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)) |
4 | 3 | albii 1816 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) |
5 | 1, 4 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) |
6 | elisset 2821 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
7 | ralsng.1 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 7 | pm5.74i 271 | . . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
9 | 8 | albii 1816 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
10 | 9 | a1i 11 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))) |
11 | 19.23v 1940 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
12 | 11 | a1i 11 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
13 | pm5.5 361 | . . . 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 206 ∀wal 1535 = wceq 1537 ∃wex 1776 ∈ wcel 2106 ∀wral 3059 {csn 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-v 3480 df-sn 4632 |
This theorem is referenced by: rexsng 4681 2ralsng 4683 ralsn 4686 ralprg 4701 raltpg 4703 ralunsn 4899 iinxsng 5093 frirr 5665 posn 5774 frsn 5776 f1ounsn 7292 f12dfv 7293 naddov2 8716 naddunif 8730 naddasslem1 8731 naddasslem2 8732 ranksnb 9865 mgm1 18684 sgrp1 18755 mnd1 18805 grp1 19078 cntzsnval 19355 abl1 19899 srgbinomlem4 20247 ring1 20324 mat1dimmul 22498 ufileu 23943 istrkg3ld 28484 1hevtxdg0 29538 wlkp1lem8 29713 wwlksnext 29923 wwlksext2clwwlk 30086 dfconngr1 30217 1conngr 30223 frgr1v 30300 lindssn 33386 lbslsat 33644 bj-raldifsn 37083 lindsadd 37600 poimirlem26 37633 poimirlem27 37634 poimirlem31 37638 cantnfresb 43314 safesnsupfilb 43408 cfsetsnfsetf1 47009 zlidlring 48078 linds0 48311 snlindsntor 48317 lmod1 48338 |
Copyright terms: Public domain | W3C validator |