Theorem sbcpr

Description: The proper substitution of an unordered pair for a setvar variable corresponds to a proper substitution of each of its elements. (Contributed by AV, 7-Apr-2023)

	Ref	Expression
Hypothesis	sbcpr.x	|- ( p = { x , y } -> ( ph <-> ps ) )
Assertion	sbcpr	|- ( [. { a , b } / p ]. ph <-> [. b / y ]. [. a / x ]. ps )

Proof

Step	Hyp	Ref	Expression
1		sbcpr.x	|- ( p = { x , y } -> ( ph <-> ps ) )
2		sbc5	|- ( [. { a , b } / p ]. ph <-> E. p ( p = { a , b } /\ ph ) )
3		preq12	|- ( ( x = a /\ y = b ) -> { x , y } = { a , b } )
4	3	eqcomd	|- ( ( x = a /\ y = b ) -> { a , b } = { x , y } )
5	4	eqeq2d	|- ( ( x = a /\ y = b ) -> ( p = { a , b } <-> p = { x , y } ) )
6	5	biimpa	|- ( ( ( x = a /\ y = b ) /\ p = { a , b } ) -> p = { x , y } )
7	6 1	syl	|- ( ( ( x = a /\ y = b ) /\ p = { a , b } ) -> ( ph <-> ps ) )
8	7	biimpd	|- ( ( ( x = a /\ y = b ) /\ p = { a , b } ) -> ( ph -> ps ) )
9	8	expcom	|- ( p = { a , b } -> ( ( x = a /\ y = b ) -> ( ph -> ps ) ) )
10	9	expd	|- ( p = { a , b } -> ( x = a -> ( y = b -> ( ph -> ps ) ) ) )
11	10	com24	|- ( p = { a , b } -> ( ph -> ( y = b -> ( x = a -> ps ) ) ) )
12	11	imp31	|- ( ( ( p = { a , b } /\ ph ) /\ y = b ) -> ( x = a -> ps ) )
13	12	alrimiv	|- ( ( ( p = { a , b } /\ ph ) /\ y = b ) -> A. x ( x = a -> ps ) )
14		vex	|- a e. _V
15	14	sbc6	|- ( [. a / x ]. ps <-> A. x ( x = a -> ps ) )
16	13 15	sylibr	|- ( ( ( p = { a , b } /\ ph ) /\ y = b ) -> [. a / x ]. ps )
17	16	ex	|- ( ( p = { a , b } /\ ph ) -> ( y = b -> [. a / x ]. ps ) )
18	17	alrimiv	|- ( ( p = { a , b } /\ ph ) -> A. y ( y = b -> [. a / x ]. ps ) )
19		vex	|- b e. _V
20	19	sbc6	|- ( [. b / y ]. [. a / x ]. ps <-> A. y ( y = b -> [. a / x ]. ps ) )
21	18 20	sylibr	|- ( ( p = { a , b } /\ ph ) -> [. b / y ]. [. a / x ]. ps )
22	21	exlimiv	|- ( E. p ( p = { a , b } /\ ph ) -> [. b / y ]. [. a / x ]. ps )
23	2 22	sylbi	|- ( [. { a , b } / p ]. ph -> [. b / y ]. [. a / x ]. ps )
24		sbc5	|- ( [. b / y ]. [. a / x ]. ps <-> E. y ( y = b /\ [. a / x ]. ps ) )
25		sbc5	|- ( [. a / x ]. ps <-> E. x ( x = a /\ ps ) )
26	1	bicomd	|- ( p = { x , y } -> ( ps <-> ph ) )
27	6 26	syl	|- ( ( ( x = a /\ y = b ) /\ p = { a , b } ) -> ( ps <-> ph ) )
28	27	biimpd	|- ( ( ( x = a /\ y = b ) /\ p = { a , b } ) -> ( ps -> ph ) )
29	28	expcom	|- ( p = { a , b } -> ( ( x = a /\ y = b ) -> ( ps -> ph ) ) )
30	29	com13	|- ( ps -> ( ( x = a /\ y = b ) -> ( p = { a , b } -> ph ) ) )
31	30	expd	|- ( ps -> ( x = a -> ( y = b -> ( p = { a , b } -> ph ) ) ) )
32	31	impcom	|- ( ( x = a /\ ps ) -> ( y = b -> ( p = { a , b } -> ph ) ) )
33	32	exlimiv	|- ( E. x ( x = a /\ ps ) -> ( y = b -> ( p = { a , b } -> ph ) ) )
34	25 33	sylbi	|- ( [. a / x ]. ps -> ( y = b -> ( p = { a , b } -> ph ) ) )
35	34	impcom	|- ( ( y = b /\ [. a / x ]. ps ) -> ( p = { a , b } -> ph ) )
36	35	exlimiv	|- ( E. y ( y = b /\ [. a / x ]. ps ) -> ( p = { a , b } -> ph ) )
37	24 36	sylbi	|- ( [. b / y ]. [. a / x ]. ps -> ( p = { a , b } -> ph ) )
38	37	alrimiv	|- ( [. b / y ]. [. a / x ]. ps -> A. p ( p = { a , b } -> ph ) )
39		prex	|- { a , b } e. _V
40	39	sbc6	|- ( [. { a , b } / p ]. ph <-> A. p ( p = { a , b } -> ph ) )
41	38 40	sylibr	|- ( [. b / y ]. [. a / x ]. ps -> [. { a , b } / p ]. ph )
42	23 41	impbii	|- ( [. { a , b } / p ]. ph <-> [. b / y ]. [. a / x ]. ps )