Step | Hyp | Ref
| Expression |
1 | | setindtr 40501 |
. . 3
⊢
(∀𝑎(𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) → (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑})) |
2 | | dfss3 3879 |
. . . 4
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑}) |
3 | | nfcv 2900 |
. . . . . . 7
⊢
Ⅎ𝑥𝑎 |
4 | | nfsab1 2721 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} |
5 | 3, 4 | nfralw 3140 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} |
6 | | nfsab1 2721 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 ∈ {𝑥 ∣ 𝜑} |
7 | 5, 6 | nfim 1904 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
8 | | raleq 3312 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑})) |
9 | | eleq1w 2816 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑎 ∈ {𝑥 ∣ 𝜑})) |
10 | 8, 9 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) ↔ (∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}))) |
11 | | setindtrs.a |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝜓 → 𝜑) |
12 | | vex 3405 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
13 | | setindtrs.b |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
14 | 12, 13 | elab 3580 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
15 | 14 | ralbii 3081 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑥 𝜓) |
16 | | abid 2716 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
17 | 11, 15, 16 | 3imtr4i 295 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) |
18 | 7, 10, 17 | chvarfv 2238 |
. . . 4
⊢
(∀𝑦 ∈
𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
19 | 2, 18 | sylbi 220 |
. . 3
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
20 | 1, 19 | mpg 1805 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑}) |
21 | | elex 3419 |
. . . . 5
⊢ (𝐵 ∈ 𝑧 → 𝐵 ∈ V) |
22 | 21 | adantl 485 |
. . . 4
⊢ ((Tr
𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
23 | 22 | exlimiv 1938 |
. . 3
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
24 | | setindtrs.c |
. . . 4
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
25 | 24 | elabg 3578 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
26 | 23, 25 | syl 17 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
27 | 20, 26 | mpbid 235 |
1
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒) |