Step | Hyp | Ref
| Expression |
1 | | ancrb 540 |
. . 3
⊢ ((𝜑 → 𝑥 ∈ 𝐴) ↔ (𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) |
2 | 1 | albii 1782 |
. 2
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) |
3 | | nfv 1873 |
. . 3
⊢
Ⅎ𝑦(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) |
4 | | nfsab1 2761 |
. . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} |
5 | | nfrab1 3318 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} |
6 | 5 | nfcri 2920 |
. . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} |
7 | 4, 6 | nfim 1859 |
. . 3
⊢
Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) |
8 | | abid 2756 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
9 | | eleq1w 2842 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) |
10 | 8, 9 | syl5bbr 277 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) |
11 | | rabid 3311 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) |
12 | | eleq1w 2842 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
13 | 11, 12 | syl5bbr 277 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
14 | 10, 13 | imbi12d 337 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}))) |
15 | 3, 7, 14 | cbvalv1 2277 |
. 2
⊢
(∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
16 | | eqss 3867 |
. . 3
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
17 | | rabssab 3944 |
. . . 4
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} |
18 | 17 | biantrur 523 |
. . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
19 | | dfss2 3840 |
. . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
20 | 16, 18, 19 | 3bitr2ri 292 |
. 2
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) |
21 | 2, 15, 20 | 3bitri 289 |
1
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) |