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 { 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 2 }

Proof

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