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 preq2 b = Y A b = A Y
3 2 eqeq2d b = Y X Y = A b X Y = A Y
4 3 adantl A = X X V Y V b = Y X Y = A b X Y = A Y
5 preq1 X = A X Y = A Y
6 5 eqcoms A = X X Y = A Y
7 6 adantr A = X X V Y V X Y = A Y
8 1 4 7 rspcedvd A = X X V Y V b V X Y = A b
9 8 ex A = X X V Y V b V X Y = A b
10 simprl A = Y X V Y V X V
11 preq2 b = X A b = A X
12 11 eqeq2d b = X X Y = A b X Y = A X
13 12 adantl A = Y X V Y V b = X X Y = A b X Y = A X
14 preq2 Y = A X Y = X A
15 14 eqcoms A = Y X Y = X A
16 prcom X A = A X
17 15 16 eqtrdi A = Y X Y = A X
18 17 adantr A = Y X V Y V X Y = A X
19 10 13 18 rspcedvd A = Y X V Y V b V X Y = A b
20 19 ex A = Y X V Y V b V X Y = A b
21 9 20 jaoi A = X A = Y X V Y V b V X Y = A b
22 elpri A X Y A = X A = Y
23 21 22 syl11 X V Y V A X Y b V X Y = A b
24 23 3impia X V Y V A X Y b V X Y = A b