Step | Hyp | Ref
| Expression |
1 | | setindtr 39499 |
. . 3
⊢
(∀𝑎(𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) → (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑})) |
2 | | dfss3 3953 |
. . . 4
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑}) |
3 | | nfcv 2974 |
. . . . . . 7
⊢
Ⅎ𝑥𝑎 |
4 | | nfsab1 2805 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} |
5 | 3, 4 | nfralw 3222 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} |
6 | | nfsab1 2805 |
. . . . . 6
⊢
Ⅎ𝑥 𝑎 ∈ {𝑥 ∣ 𝜑} |
7 | 5, 6 | nfim 1888 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
8 | | raleq 3403 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑})) |
9 | | eleq1w 2892 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑎 ∈ {𝑥 ∣ 𝜑})) |
10 | 8, 9 | imbi12d 346 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) ↔ (∀𝑦 ∈ 𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}))) |
11 | | setindtrs.a |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝜓 → 𝜑) |
12 | | vex 3495 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
13 | | setindtrs.b |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
14 | 12, 13 | elab 3664 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
15 | 14 | ralbii 3162 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑥 𝜓) |
16 | | abid 2800 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
17 | 11, 15, 16 | 3imtr4i 293 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑥 ∈ {𝑥 ∣ 𝜑}) |
18 | 7, 10, 17 | chvarfv 2232 |
. . . 4
⊢
(∀𝑦 ∈
𝑎 𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
19 | 2, 18 | sylbi 218 |
. . 3
⊢ (𝑎 ⊆ {𝑥 ∣ 𝜑} → 𝑎 ∈ {𝑥 ∣ 𝜑}) |
20 | 1, 19 | mpg 1789 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ {𝑥 ∣ 𝜑}) |
21 | | elex 3510 |
. . . . 5
⊢ (𝐵 ∈ 𝑧 → 𝐵 ∈ V) |
22 | 21 | adantl 482 |
. . . 4
⊢ ((Tr
𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
23 | 22 | exlimiv 1922 |
. . 3
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝐵 ∈ V) |
24 | | setindtrs.c |
. . . 4
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
25 | 24 | elabg 3663 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
26 | 23, 25 | syl 17 |
. 2
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → (𝐵 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
27 | 20, 26 | mpbid 233 |
1
⊢
(∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒) |