Step |
Hyp |
Ref |
Expression |
1 |
|
eleq12 |
⊢ ( ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∧ 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) → ( 𝑦 ∈ 𝑦 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
2 |
1
|
anidms |
⊢ ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( 𝑦 ∈ 𝑦 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
3 |
2
|
notbid |
⊢ ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( ¬ 𝑦 ∈ 𝑦 ↔ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
4 |
|
eleq12 |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) ) |
5 |
4
|
anidms |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) ) |
6 |
5
|
notbid |
⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦 ) ) |
7 |
6
|
cbvrabv |
⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } = { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 } |
8 |
3 7
|
elrab2 |
⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) |
9 |
|
pclem6 |
⊢ ( ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ) |
10 |
8 9
|
ax-mp |
⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 |