![]() |
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 3853. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.) |
Ref | Expression |
---|---|
sbcg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 3777 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | dfclel 2804 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
3 | df-clab 2704 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
4 | sbv 2084 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | |
5 | 3, 4 | bitri 274 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
6 | 5 | anbi2i 621 | . . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑)) |
7 | 6 | exbii 1843 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)) |
8 | 1, 2, 7 | 3bitrri 297 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑) |
9 | dfclel 2804 | . . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) | |
10 | 9 | biimpi 215 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) |
11 | simpr 483 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) | |
12 | 11 | ax-gen 1790 | . . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) |
13 | 19.23v 1938 | . . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) | |
14 | 13 | biimpi 215 | . . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
15 | 12, 14 | mp1i 13 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
16 | 2a1 28 | . . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴))) | |
17 | 16 | imp 405 | . . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴)) |
18 | 17 | ancrd 550 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
19 | 18 | eximi 1830 | . . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
20 | 19.37imv 1944 | . . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) | |
21 | 19, 20 | syl 17 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) |
22 | 15, 21 | impbid 211 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
23 | 10, 22 | syl 17 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
24 | 8, 23 | bitr3id 284 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1532 = wceq 1534 ∃wex 1774 [wsb 2060 ∈ wcel 2099 {cab 2703 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-clel 2803 df-sbc 3777 |
This theorem is referenced by: sbcabel 3871 csbconstg 3911 2nreu 4446 csbuni 4944 csbxp 5781 sbcfung 6583 fmptsnd 7183 csbfrecsg 8299 opsbc2ie 32404 f1od2 32635 bnj89 34566 bnj525 34583 bnj1128 34835 csbrdgg 37036 csboprabg 37037 mptsnunlem 37045 topdifinffinlem 37054 relowlpssretop 37071 rdgeqoa 37077 csbfinxpg 37095 gm-sbtru 37807 sbfal 37808 cdlemk40 40616 cdlemkid3N 40632 cdlemkid4 40633 frege70 43600 frege77 43607 frege116 43646 frege118 43648 trsbc 44216 trsbcVD 44553 csbxpgVD 44570 csbunigVD 44574 |
Copyright terms: Public domain | W3C validator |