This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prprrab

Description: The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020)

Ref Expression
Assertion prprrab ⊢ x ∈ 𝒫 A ∖ ∅ | x = 2 = x ∈ 𝒫 A | x = 2

Proof

Step Hyp Ref Expression
1 2ne0 ⊢ 2 ≠ 0
2 1 neii ⊢ ¬ 2 = 0
3 eqeq1 ⊢ x = 2 → x = 0 ↔ 2 = 0
4 2 3 mtbiri ⊢ x = 2 → ¬ x = 0
5 hasheq0 ⊢ x ∈ V → x = 0 ↔ x = ∅
6 5 bicomd ⊢ x ∈ V → x = ∅ ↔ x = 0
7 6 necon3abid ⊢ x ∈ V → x ≠ ∅ ↔ ¬ x = 0
8 7 elv ⊢ x ≠ ∅ ↔ ¬ x = 0
9 4 8 sylibr ⊢ x = 2 → x ≠ ∅
10 9 biantrud ⊢ x = 2 → x ∈ 𝒫 A ↔ x ∈ 𝒫 A ∧ x ≠ ∅
11 eldifsn ⊢ x ∈ 𝒫 A ∖ ∅ ↔ x ∈ 𝒫 A ∧ x ≠ ∅
12 10 11 bitr4di ⊢ x = 2 → x ∈ 𝒫 A ↔ x ∈ 𝒫 A ∖ ∅
13 12 pm5.32ri ⊢ x ∈ 𝒫 A ∧ x = 2 ↔ x ∈ 𝒫 A ∖ ∅ ∧ x = 2
14 13 abbii ⊢ x | x ∈ 𝒫 A ∧ x = 2 = x | x ∈ 𝒫 A ∖ ∅ ∧ x = 2
15 df-rab ⊢ x ∈ 𝒫 A | x = 2 = x | x ∈ 𝒫 A ∧ x = 2
16 df-rab ⊢ x ∈ 𝒫 A ∖ ∅ | x = 2 = x | x ∈ 𝒫 A ∖ ∅ ∧ x = 2
17 14 15 16 3eqtr4ri ⊢ x ∈ 𝒫 A ∖ ∅ | x = 2 = x ∈ 𝒫 A | x = 2