Theorem exprelprel

Description: If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018)

	Ref	Expression
Assertion	exprelprel	|- ( E. p e. { e e. ~P V | ( # ` e ) = 2 } p e. X -> E. v e. V E. w e. V { v , w } e. X )

Proof

Step	Hyp	Ref	Expression
1		elss2prb	|- ( p e. { e e. ~P V | ( # ` e ) = 2 } <-> E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) )
2		eleq1	|- ( p = { v , w } -> ( p e. X <-> { v , w } e. X ) )
3	2	adantl	|- ( ( v =/= w /\ p = { v , w } ) -> ( p e. X <-> { v , w } e. X ) )
4	3	biimpcd	|- ( p e. X -> ( ( v =/= w /\ p = { v , w } ) -> { v , w } e. X ) )
5	4	reximdv	|- ( p e. X -> ( E. w e. V ( v =/= w /\ p = { v , w } ) -> E. w e. V { v , w } e. X ) )
6	5	reximdv	|- ( p e. X -> ( E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) -> E. v e. V E. w e. V { v , w } e. X ) )
7	6	com12	|- ( E. v e. V E. w e. V ( v =/= w /\ p = { v , w } ) -> ( p e. X -> E. v e. V E. w e. V { v , w } e. X ) )
8	1 7	sylbi	|- ( p e. { e e. ~P V | ( # ` e ) = 2 } -> ( p e. X -> E. v e. V E. w e. V { v , w } e. X ) )
9	8	rexlimiv	|- ( E. p e. { e e. ~P V | ( # ` e ) = 2 } p e. X -> E. v e. V E. w e. V { v , w } e. X )