![]() |
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 3855. (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 3779 | . . 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 3778 |
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 3779 |
This theorem is referenced by: sbcabel 3873 csbconstg 3913 2nreu 4442 csbuni 4941 csbxp 5776 sbcfung 6573 fmptsnd 7167 csbfrecsg 8269 opsbc2ie 31716 f1od2 31946 bnj89 33732 bnj525 33749 bnj1128 34001 csbrdgg 36210 csboprabg 36211 mptsnunlem 36219 topdifinffinlem 36228 relowlpssretop 36245 rdgeqoa 36251 csbfinxpg 36269 gm-sbtru 36974 sbfal 36975 cdlemk40 39788 cdlemkid3N 39804 cdlemkid4 39805 frege70 42684 frege77 42691 frege116 42730 frege118 42732 trsbc 43301 trsbcVD 43638 csbxpgVD 43655 csbunigVD 43659 |
Copyright terms: Public domain | W3C validator |