Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > repizf2 | GIF version |
Description: Replacement. This version of replacement is stronger than repizf 3894 in the sense that 𝜑 does not need to map all values of 𝑥 in 𝑤 to a value of 𝑦. The resulting set contains those elements for which there is a value of 𝑦 and in that sense, this theorem combines repizf 3894 with ax-sep 3896. Another variation would be ∀𝑥 ∈ 𝑤∃*𝑦𝜑 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)} ∈ V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Ref | Expression |
---|---|
repizf2.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
repizf2 | ⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2604 | . . 3 ⊢ 𝑤 ∈ V | |
2 | 1 | rabex 3922 | . 2 ⊢ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} ∈ V |
3 | repizf2lem 3935 | . . . 4 ⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 ↔ ∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃!𝑦𝜑) | |
4 | nfcv 2219 | . . . . . 6 ⊢ Ⅎ𝑥𝑣 | |
5 | nfrab1 2533 | . . . . . 6 ⊢ Ⅎ𝑥{𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} | |
6 | 4, 5 | raleqf 2545 | . . . . 5 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∀𝑥 ∈ 𝑣 ∃!𝑦𝜑 ↔ ∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃!𝑦𝜑)) |
7 | repizf2.1 | . . . . . 6 ⊢ Ⅎ𝑧𝜑 | |
8 | 7 | repizf 3894 | . . . . 5 ⊢ (∀𝑥 ∈ 𝑣 ∃!𝑦𝜑 → ∃𝑧∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑧 𝜑) |
9 | 6, 8 | syl6bir 162 | . . . 4 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃!𝑦𝜑 → ∃𝑧∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑧 𝜑)) |
10 | 3, 9 | syl5bi 150 | . . 3 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑧 𝜑)) |
11 | df-rab 2357 | . . . . . 6 ⊢ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑤 ∧ ∃𝑦𝜑)} | |
12 | nfv 1461 | . . . . . . . 8 ⊢ Ⅎ𝑧 𝑥 ∈ 𝑤 | |
13 | 7 | nfex 1568 | . . . . . . . 8 ⊢ Ⅎ𝑧∃𝑦𝜑 |
14 | 12, 13 | nfan 1497 | . . . . . . 7 ⊢ Ⅎ𝑧(𝑥 ∈ 𝑤 ∧ ∃𝑦𝜑) |
15 | 14 | nfab 2223 | . . . . . 6 ⊢ Ⅎ𝑧{𝑥 ∣ (𝑥 ∈ 𝑤 ∧ ∃𝑦𝜑)} |
16 | 11, 15 | nfcxfr 2216 | . . . . 5 ⊢ Ⅎ𝑧{𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} |
17 | 16 | nfeq2 2230 | . . . 4 ⊢ Ⅎ𝑧 𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} |
18 | 4, 5 | raleqf 2545 | . . . 4 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑)) |
19 | 17, 18 | exbid 1547 | . . 3 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∃𝑧∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑)) |
20 | 10, 19 | sylibd 147 | . 2 ⊢ (𝑣 = {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑} → (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑)) |
21 | 2, 20 | vtocle 2672 | 1 ⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = wceq 1284 Ⅎwnf 1389 ∃wex 1421 ∃!weu 1941 ∃*wmo 1942 {cab 2067 ∀wral 2348 ∃wrex 2349 {crab 2352 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 ax-coll 3893 ax-sep 3896 |
This theorem depends on definitions: df-bi 115 df-tru 1287 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-ral 2353 df-rab 2357 df-v 2603 df-in 2979 df-ss 2986 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |