Metamath Proof Explorer


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 φ ψ
Assertion sbcpr [˙ a b / p]˙ φ [˙b / y]˙ [˙a / x]˙ ψ

Proof

Step Hyp Ref Expression
1 sbcpr.x p = x y φ ψ
2 sbc5 [˙ a b / p]˙ φ p p = a b φ
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 φ ψ
8 7 biimpd x = a y = b p = a b φ ψ
9 8 expcom p = a b x = a y = b φ ψ
10 9 expd p = a b x = a y = b φ ψ
11 10 com24 p = a b φ y = b x = a ψ
12 11 imp31 p = a b φ y = b x = a ψ
13 12 alrimiv p = a b φ y = b x x = a ψ
14 vex a V
15 14 sbc6 [˙a / x]˙ ψ x x = a ψ
16 13 15 sylibr p = a b φ y = b [˙a / x]˙ ψ
17 16 ex p = a b φ y = b [˙a / x]˙ ψ
18 17 alrimiv p = a b φ y y = b [˙a / x]˙ ψ
19 vex b V
20 19 sbc6 [˙b / y]˙ [˙a / x]˙ ψ y y = b [˙a / x]˙ ψ
21 18 20 sylibr p = a b φ [˙b / y]˙ [˙a / x]˙ ψ
22 21 exlimiv p p = a b φ [˙b / y]˙ [˙a / x]˙ ψ
23 2 22 sylbi [˙ a b / p]˙ φ [˙b / y]˙ [˙a / x]˙ ψ
24 sbc5 [˙b / y]˙ [˙a / x]˙ ψ y y = b [˙a / x]˙ ψ
25 sbc5 [˙a / x]˙ ψ x x = a ψ
26 1 bicomd p = x y ψ φ
27 6 26 syl x = a y = b p = a b ψ φ
28 27 biimpd x = a y = b p = a b ψ φ
29 28 expcom p = a b x = a y = b ψ φ
30 29 com13 ψ x = a y = b p = a b φ
31 30 expd ψ x = a y = b p = a b φ
32 31 impcom x = a ψ y = b p = a b φ
33 32 exlimiv x x = a ψ y = b p = a b φ
34 25 33 sylbi [˙a / x]˙ ψ y = b p = a b φ
35 34 impcom y = b [˙a / x]˙ ψ p = a b φ
36 35 exlimiv y y = b [˙a / x]˙ ψ p = a b φ
37 24 36 sylbi [˙b / y]˙ [˙a / x]˙ ψ p = a b φ
38 37 alrimiv [˙b / y]˙ [˙a / x]˙ ψ p p = a b φ
39 prex a b V
40 39 sbc6 [˙ a b / p]˙ φ p p = a b φ
41 38 40 sylibr [˙b / y]˙ [˙a / x]˙ ψ [˙ a b / p]˙ φ
42 23 41 impbii [˙ a b / p]˙ φ [˙b / y]˙ [˙a / x]˙ ψ