Step | Hyp | Ref
| Expression |
1 | | setindtr 36609 |
. . 3
⊢
(∀𝑎(𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) → (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑})) |
2 | | dfss3 3558 |
. . . 4
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑}) |
3 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑎 |
4 | | nfsab1 2600 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} |
5 | 3, 4 | nfral 2929 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} |
6 | | nfsab1 2600 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 ∈ {𝑥 ∣ 𝜑} |
7 | 5, 6 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
8 | | raleq 3115 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑})) |
9 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑎 ∈ {𝑥 ∣ 𝜑})) |
10 | 8, 9 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) ↔ (∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}))) |
11 | | setindtrs.a |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝜓 → 𝜑) |
12 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
13 | | setindtrs.b |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
14 | 12, 13 | elab 3319 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
15 | 14 | ralbii 2963 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑥 𝜓) |
16 | | abid 2598 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
17 | 11, 15, 16 | 3imtr4i 280 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) |
18 | 7, 10, 17 | chvar 2250 |
. . . 4
⊢
(∀𝑦 ∈
𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
19 | 2, 18 | sylbi 206 |
. . 3
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
20 | 1, 19 | mpg 1715 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑}) |
21 | | elex 3185 |
. . . . 5
⊢ (𝐵 ∈ 𝑧 → 𝐵 ∈ V) |
22 | 21 | adantl 481 |
. . . 4
⊢ ((Tr
𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
23 | 22 | exlimiv 1845 |
. . 3
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
24 | | setindtrs.c |
. . . 4
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
25 | 24 | elabg 3320 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
26 | 23, 25 | syl 17 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
27 | 20, 26 | mpbid 221 |
1
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒) |