![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcg | Structured version Visualization version GIF version |
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3854. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024.) |
Ref | Expression |
---|---|
sbcg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 3778 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | dfclel 2812 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
3 | df-clab 2711 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
4 | sbv 2092 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | |
5 | 3, 4 | bitri 275 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
6 | 5 | anbi2i 624 | . . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑)) |
7 | 6 | exbii 1851 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)) |
8 | 1, 2, 7 | 3bitrri 298 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑) |
9 | dfclel 2812 | . . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) | |
10 | 9 | biimpi 215 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) |
11 | simpr 486 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) | |
12 | 11 | ax-gen 1798 | . . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) |
13 | 19.23v 1946 | . . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) | |
14 | 13 | biimpi 215 | . . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
15 | 12, 14 | mp1i 13 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
16 | 2a1 28 | . . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴))) | |
17 | 16 | imp 408 | . . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴)) |
18 | 17 | ancrd 553 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
19 | 18 | eximi 1838 | . . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
20 | 19.37imv 1952 | . . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) | |
21 | 19, 20 | syl 17 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) |
22 | 15, 21 | impbid 211 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
23 | 10, 22 | syl 17 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
24 | 8, 23 | bitr3id 285 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∃wex 1782 [wsb 2068 ∈ wcel 2107 {cab 2710 [wsbc 3777 |
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 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-clel 2811 df-sbc 3778 |
This theorem is referenced by: sbcabel 3872 csbconstg 3912 2nreu 4441 csbuni 4940 csbxp 5774 sbcfung 6570 fmptsnd 7164 csbfrecsg 8266 opsbc2ie 31704 f1od2 31934 bnj89 33721 bnj525 33738 bnj1128 33990 csbrdgg 36199 csboprabg 36200 mptsnunlem 36208 topdifinffinlem 36217 relowlpssretop 36234 rdgeqoa 36240 csbfinxpg 36258 gm-sbtru 36963 sbfal 36964 cdlemk40 39777 cdlemkid3N 39793 cdlemkid4 39794 frege70 42670 frege77 42677 frege116 42716 frege118 42718 trsbc 43287 trsbcVD 43624 csbxpgVD 43641 csbunigVD 43645 |
Copyright terms: Public domain | W3C validator |