Metamath Proof Explorer


Theorem elpr2elpr

Description: For an element A of an unordered pair which is a subset of a given set V , there is another (maybe the same) element b of the given set V being an element of the unordered pair. (Contributed by AV, 5-Dec-2020)

Ref Expression
Assertion elpr2elpr X V Y V A X Y b V X Y = A b

Proof

Step Hyp Ref Expression
1 simprr A = X X V Y V Y V
2 preq12 A = X b = Y A b = X Y
3 2 eqcomd A = X b = Y X Y = A b
4 3 adantlr A = X X V Y V b = Y X Y = A b
5 1 4 rspcedeq2vd A = X X V Y V b V X Y = A b
6 5 ex A = X X V Y V b V X Y = A b
7 simprl A = Y X V Y V X V
8 preq12 A = Y b = X A b = Y X
9 prcom Y X = X Y
10 8 9 eqtr2di A = Y b = X X Y = A b
11 10 adantlr A = Y X V Y V b = X X Y = A b
12 7 11 rspcedeq2vd A = Y X V Y V b V X Y = A b
13 12 ex A = Y X V Y V b V X Y = A b
14 6 13 jaoi A = X A = Y X V Y V b V X Y = A b
15 elpri A X Y A = X A = Y
16 14 15 syl11 X V Y V A X Y b V X Y = A b
17 16 3impia X V Y V A X Y b V X Y = A b