| 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 3861. (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 3789 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
| 2 | dfclel 2817 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
| 3 | df-clab 2715 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
| 4 | sbv 2088 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | |
| 5 | 3, 4 | bitri 275 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
| 6 | 5 | anbi2i 623 | . . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑)) |
| 7 | 6 | exbii 1848 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)) |
| 8 | 1, 2, 7 | 3bitrri 298 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑) |
| 9 | dfclel 2817 | . . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) | |
| 10 | 9 | biimpi 216 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) |
| 11 | simpr 484 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) | |
| 12 | 11 | ax-gen 1795 | . . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) |
| 13 | 19.23v 1942 | . . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) | |
| 14 | 13 | biimpi 216 | . . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
| 15 | 12, 14 | mp1i 13 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑)) |
| 16 | 2a1 28 | . . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴))) | |
| 17 | 16 | imp 406 | . . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴)) |
| 18 | 17 | ancrd 551 | . . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
| 19 | 18 | eximi 1835 | . . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑))) |
| 20 | 19.37imv 1947 | . . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) | |
| 21 | 19, 20 | syl 17 | . . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))) |
| 22 | 15, 21 | impbid 212 | . . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
| 23 | 10, 22 | syl 17 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑)) |
| 24 | 8, 23 | bitr3id 285 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃wex 1779 [wsb 2064 ∈ wcel 2108 {cab 2714 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: sbcabel 3878 csbconstg 3918 2nreu 4444 csbuni 4936 csbxp 5785 sbcfung 6590 fmptsnd 7189 csbfrecsg 8309 opsbc2ie 32495 f1od2 32732 bnj89 34735 bnj525 34752 bnj1128 35004 csbrdgg 37330 csboprabg 37331 mptsnunlem 37339 topdifinffinlem 37348 relowlpssretop 37365 rdgeqoa 37371 csbfinxpg 37389 gm-sbtru 38113 sbfal 38114 cdlemk40 40919 cdlemkid3N 40935 cdlemkid4 40936 frege70 43946 frege77 43953 frege116 43992 frege118 43994 trsbc 44560 trsbcVD 44897 csbxpgVD 44914 csbunigVD 44918 |
| Copyright terms: Public domain | W3C validator |