Theorem elpreqpr

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

	Ref	Expression
Assertion	elpreqpr	|- ( A e. { B , C } -> E. x { B , C } = { A , x } )

Proof

Step	Hyp	Ref	Expression
1		elpri	|- ( A e. { B , C } -> ( A = B \/ A = C ) )
2		elex	|- ( A e. { B , C } -> A e. _V )
3		elpreqprlem	|- ( B e. _V -> E. x { B , C } = { B , x } )
4		eleq1	|- ( A = B -> ( A e. _V <-> B e. _V ) )
5		preq1	|- ( A = B -> { A , x } = { B , x } )
6	5	eqeq2d	|- ( A = B -> ( { B , C } = { A , x } <-> { B , C } = { B , x } ) )
7	6	exbidv	|- ( A = B -> ( E. x { B , C } = { A , x } <-> E. x { B , C } = { B , x } ) )
8	4 7	imbi12d	|- ( A = B -> ( ( A e. _V -> E. x { B , C } = { A , x } ) <-> ( B e. _V -> E. x { B , C } = { B , x } ) ) )
9	3 8	mpbiri	|- ( A = B -> ( A e. _V -> E. x { B , C } = { A , x } ) )
10	9	imp	|- ( ( A = B /\ A e. _V ) -> E. x { B , C } = { A , x } )
11		elpreqprlem	|- ( C e. _V -> E. x { C , B } = { C , x } )
12		prcom	|- { C , B } = { B , C }
13	12	eqeq1i	|- ( { C , B } = { C , x } <-> { B , C } = { C , x } )
14	13	exbii	|- ( E. x { C , B } = { C , x } <-> E. x { B , C } = { C , x } )
15	11 14	sylib	|- ( C e. _V -> E. x { B , C } = { C , x } )
16		eleq1	|- ( A = C -> ( A e. _V <-> C e. _V ) )
17		preq1	|- ( A = C -> { A , x } = { C , x } )
18	17	eqeq2d	|- ( A = C -> ( { B , C } = { A , x } <-> { B , C } = { C , x } ) )
19	18	exbidv	|- ( A = C -> ( E. x { B , C } = { A , x } <-> E. x { B , C } = { C , x } ) )
20	16 19	imbi12d	|- ( A = C -> ( ( A e. _V -> E. x { B , C } = { A , x } ) <-> ( C e. _V -> E. x { B , C } = { C , x } ) ) )
21	15 20	mpbiri	|- ( A = C -> ( A e. _V -> E. x { B , C } = { A , x } ) )
22	21	imp	|- ( ( A = C /\ A e. _V ) -> E. x { B , C } = { A , x } )
23	10 22	jaoian	|- ( ( ( A = B \/ A = C ) /\ A e. _V ) -> E. x { B , C } = { A , x } )
24	1 2 23	syl2anc	|- ( A e. { B , C } -> E. x { B , C } = { A , x } )