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 }