Metamath Proof Explorer


Theorem elpreqpr

Description: Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020)

Ref Expression
Assertion elpreqpr ABCxBC=Ax

Proof

Step Hyp Ref Expression
1 elpri ABCA=BA=C
2 elex ABCAV
3 elpreqprlem BVxBC=Bx
4 eleq1 A=BAVBV
5 preq1 A=BAx=Bx
6 5 eqeq2d A=BBC=AxBC=Bx
7 6 exbidv A=BxBC=AxxBC=Bx
8 4 7 imbi12d A=BAVxBC=AxBVxBC=Bx
9 3 8 mpbiri A=BAVxBC=Ax
10 9 imp A=BAVxBC=Ax
11 elpreqprlem CVxCB=Cx
12 prcom CB=BC
13 12 eqeq1i CB=CxBC=Cx
14 13 exbii xCB=CxxBC=Cx
15 11 14 sylib CVxBC=Cx
16 eleq1 A=CAVCV
17 preq1 A=CAx=Cx
18 17 eqeq2d A=CBC=AxBC=Cx
19 18 exbidv A=CxBC=AxxBC=Cx
20 16 19 imbi12d A=CAVxBC=AxCVxBC=Cx
21 15 20 mpbiri A=CAVxBC=Ax
22 21 imp A=CAVxBC=Ax
23 10 22 jaoian A=BA=CAVxBC=Ax
24 1 2 23 syl2anc ABCxBC=Ax