![]() |
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 3477 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2139. (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 2895 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
3 | cbvrabw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
4 | 2, 3 | nfan 1897 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) |
5 | cbvrabw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
6 | 5 | nfcri 2895 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
7 | cbvrabw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
8 | 6, 7 | nfan 1897 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜓) |
9 | eleq1w 2822 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
10 | cbvrabw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
11 | 9, 10 | anbi12d 632 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
12 | 4, 8, 11 | cbvabw 2811 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
13 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
14 | df-rab 3434 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
15 | 12, 13, 14 | 3eqtr4i 2773 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 Ⅎwnf 1780 ∈ wcel 2106 {cab 2712 Ⅎwnfc 2888 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-rab 3434 |
This theorem is referenced by: elrabsf 3840 f1ossf1o 7148 tfis 7876 cantnflem1 9727 scottexs 9925 scott0s 9926 elmptrab 23851 bnj1534 34846 scottexf 38155 scott0f 38156 aks6d1c7lem3 42164 unitscyglem3 42179 unitscyglem4 42180 eq0rabdioph 42764 rexrabdioph 42782 rexfrabdioph 42783 elnn0rabdioph 42791 dvdsrabdioph 42798 binomcxplemdvsum 44351 fnlimcnv 45623 fnlimabslt 45635 stoweidlem34 45990 stoweidlem59 46015 pimltmnf2f 46653 pimgtpnf2f 46661 pimltpnf2f 46668 issmff 46690 smfpimltxrmptf 46714 smfpreimagtf 46724 smflim 46733 smfpimgtxr 46736 smfpimgtxrmptf 46740 smflim2 46762 smflimsup 46784 smfliminf 46787 |
Copyright terms: Public domain | W3C validator |