| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvrabw | Structured version Visualization version GIF version | ||
| Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3479 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2141. (Revised by Wolf Lammen, 19-Jul-2025.) |
| Ref | Expression |
|---|---|
| cbvrabw.1 | ⊢ Ⅎ𝑥𝐴 |
| cbvrabw.2 | ⊢ Ⅎ𝑦𝐴 |
| cbvrabw.3 | ⊢ Ⅎ𝑦𝜑 |
| cbvrabw.4 | ⊢ Ⅎ𝑥𝜓 |
| cbvrabw.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvrabw | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvrabw.2 | . . . . 5 ⊢ Ⅎ𝑦𝐴 | |
| 2 | 1 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 3 | cbvrabw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
| 4 | 2, 3 | nfan 1899 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) |
| 5 | cbvrabw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 6 | 5 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 7 | cbvrabw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 8 | 6, 7 | nfan 1899 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜓) |
| 9 | eleq1w 2824 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
| 10 | cbvrabw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 11 | 9, 10 | anbi12d 632 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 12 | 4, 8, 11 | cbvabw 2813 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
| 13 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
| 14 | df-rab 3437 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
| 15 | 12, 13, 14 | 3eqtr4i 2775 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 {cab 2714 Ⅎwnfc 2890 {crab 3436 |
| 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 ax-9 2118 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 |
| This theorem is referenced by: elrabsf 3834 f1ossf1o 7148 tfis 7876 cantnflem1 9729 scottexs 9927 scott0s 9928 elmptrab 23835 bnj1534 34867 scottexf 38175 scott0f 38176 aks6d1c7lem3 42183 unitscyglem3 42198 unitscyglem4 42199 eq0rabdioph 42787 rexrabdioph 42805 rexfrabdioph 42806 elnn0rabdioph 42814 dvdsrabdioph 42821 binomcxplemdvsum 44374 fnlimcnv 45682 fnlimabslt 45694 stoweidlem34 46049 stoweidlem59 46074 pimltmnf2f 46712 pimgtpnf2f 46720 pimltpnf2f 46727 issmff 46749 smfpimltxrmptf 46773 smfpreimagtf 46783 smflim 46792 smfpimgtxr 46795 smfpimgtxrmptf 46799 smflim2 46821 smflimsup 46843 smfliminf 46846 |
| Copyright terms: Public domain | W3C validator |