Step | Hyp | Ref
| Expression |
1 | | ancrb 547 |
. . 3
⊢ ((𝜑 → 𝑥 ∈ 𝐴) ↔ (𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) |
2 | 1 | albii 1825 |
. 2
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) |
3 | | nfv 1920 |
. . 3
⊢
Ⅎ𝑦(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) |
4 | | nfsab1 2724 |
. . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} |
5 | | nfrab1 3315 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} |
6 | 5 | nfcri 2895 |
. . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} |
7 | 4, 6 | nfim 1902 |
. . 3
⊢
Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) |
8 | | abid 2720 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
9 | | eleq1w 2822 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) |
10 | 8, 9 | bitr3id 284 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) |
11 | | rabid 3308 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) |
12 | | eleq1w 2822 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
13 | 11, 12 | bitr3id 284 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
14 | 10, 13 | imbi12d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}))) |
15 | 3, 7, 14 | cbvalv1 2341 |
. 2
⊢
(∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
16 | | eqss 3940 |
. . 3
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
17 | | rabssab 4022 |
. . . 4
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} |
18 | 17 | biantrur 530 |
. . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
19 | | dfss2 3911 |
. . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
20 | 16, 18, 19 | 3bitr2ri 299 |
. 2
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) |
21 | 2, 15, 20 | 3bitri 296 |
1
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) |