|   | 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 2140, ax-12 2176. (Revised by GG, 30-Sep-2024.) | 
| Ref | Expression | 
|---|---|
| ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| ralsng | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-ral 3061 | . . 3 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑)) | |
| 2 | velsn 4641 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
| 3 | 2 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)) | 
| 4 | 3 | albii 1818 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) | 
| 5 | 1, 4 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) | 
| 6 | elisset 2822 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
| 7 | ralsng.1 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 8 | 7 | pm5.74i 271 | . . . . . 6 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) | 
| 9 | 8 | albii 1818 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) | 
| 10 | 9 | a1i 11 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))) | 
| 11 | 19.23v 1941 | . . . . 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 1537 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ∀wral 3060 {csn 4625 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-v 3481 df-sn 4626 | 
| This theorem is referenced by: rexsng 4675 2ralsng 4677 ralsn 4680 ralprg 4695 raltpg 4697 ralunsn 4893 iinxsng 5087 frirr 5660 posn 5770 frsn 5772 f1ounsn 7293 f12dfv 7294 naddov2 8718 naddunif 8732 naddasslem1 8733 naddasslem2 8734 ranksnb 9868 mgm1 18672 sgrp1 18743 mnd1 18793 grp1 19066 cntzsnval 19343 abl1 19885 srgbinomlem4 20227 ring1 20308 mat1dimmul 22483 ufileu 23928 istrkg3ld 28470 1hevtxdg0 29524 wlkp1lem8 29699 wwlksnext 29914 wwlksext2clwwlk 30077 dfconngr1 30208 1conngr 30214 frgr1v 30291 lindssn 33407 lbslsat 33668 bj-raldifsn 37102 lindsadd 37621 poimirlem26 37654 poimirlem27 37655 poimirlem31 37659 cantnfresb 43342 safesnsupfilb 43436 cfsetsnfsetf1 47076 zlidlring 48155 linds0 48387 snlindsntor 48393 lmod1 48414 | 
| Copyright terms: Public domain | W3C validator |