Theorem pairreueq

Description: Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023)

	Ref	Expression
Hypothesis	pairreueq.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion	pairreueq	|- ( E! p e. P ph <-> E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		pairreueq.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
2		fveqeq2	|- ( x = p -> ( ( # ` x ) = 2 <-> ( # ` p ) = 2 ) )
3	2 1	elrab2	|- ( p e. P <-> ( p e. ~P V /\ ( # ` p ) = 2 ) )
4	3	anbi1i	|- ( ( p e. P /\ ph ) <-> ( ( p e. ~P V /\ ( # ` p ) = 2 ) /\ ph ) )
5		anass	|- ( ( ( p e. ~P V /\ ( # ` p ) = 2 ) /\ ph ) <-> ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
6	4 5	bitri	|- ( ( p e. P /\ ph ) <-> ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
7	6	eubii	|- ( E! p ( p e. P /\ ph ) <-> E! p ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
8		df-reu	|- ( E! p e. P ph <-> E! p ( p e. P /\ ph ) )
9		df-reu	|- ( E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) <-> E! p ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
10	7 8 9	3bitr4i	|- ( E! p e. P ph <-> E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) )