Metamath Proof Explorer

Theorem prsssprel

Description: The elements of a pair from a subset of the set of all unordered pairs over a given set V are elements of the set V . (Contributed by AV, 21-Nov-2021)

		Ref	Expression
	Assertion	prsssprel	\|- ( ( P C_ ( Pairs ` V ) /\ { X , Y } e. P /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )

Proof

Step	Hyp	Ref	Expression
1		ssel2	\|- ( ( P C_ ( Pairs ` V ) /\ { X , Y } e. P ) -> { X , Y } e. ( Pairs ` V ) )
2		prsprel	\|- ( ( { X , Y } e. ( Pairs ` V ) /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )
3	1 2	stoic3	\|- ( ( P C_ ( Pairs ` V ) /\ { X , Y } e. P /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )

Step

Hyp

Ref

Expression

ssel2

 |-  ( ( P C_ ( Pairs ` V ) /\ { X , Y } e. P ) -> { X , Y } e. ( Pairs ` V ) )

prsprel

 |-  ( ( { X , Y } e. ( Pairs ` V ) /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )

1 2

stoic3

 |-  ( ( P C_ ( Pairs ` V ) /\ { X , Y } e. P /\ ( X e. U /\ Y e. W ) ) -> ( X e. V /\ Y e. V ) )