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	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜑 ↔ 𝜓 ) )
Assertion	sbcpr	⊢ ( [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbcpr.x	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜑 ↔ 𝜓 ) )
2		sbc5	⊢ ( [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 ↔ ∃ 𝑝 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
3		preq12	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } )
4	3	eqcomd	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { 𝑎 , 𝑏 } = { 𝑥 , 𝑦 } )
5	4	eqeq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑝 = { 𝑎 , 𝑏 } ↔ 𝑝 = { 𝑥 , 𝑦 } ) )
6	5	biimpa	⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 = { 𝑥 , 𝑦 } )
7	6 1	syl	⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝜑 ↔ 𝜓 ) )
8	7	biimpd	⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝜑 → 𝜓 ) )
9	8	expcom	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 → 𝜓 ) ) )
10	9	expd	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝑥 = 𝑎 → ( 𝑦 = 𝑏 → ( 𝜑 → 𝜓 ) ) ) )
11	10	com24	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝜑 → ( 𝑦 = 𝑏 → ( 𝑥 = 𝑎 → 𝜓 ) ) ) )
12	11	imp31	⊢ ( ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ 𝑦 = 𝑏 ) → ( 𝑥 = 𝑎 → 𝜓 ) )
13	12	alrimiv	⊢ ( ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ 𝑦 = 𝑏 ) → ∀ 𝑥 ( 𝑥 = 𝑎 → 𝜓 ) )
14		vex	⊢ 𝑎 ∈ V
15	14	sbc6	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ ∀ 𝑥 ( 𝑥 = 𝑎 → 𝜓 ) )
16	13 15	sylibr	⊢ ( ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) ∧ 𝑦 = 𝑏 ) → [ 𝑎 / 𝑥 ] 𝜓 )
17	16	ex	⊢ ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ( 𝑦 = 𝑏 → [ 𝑎 / 𝑥 ] 𝜓 ) )
18	17	alrimiv	⊢ ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) → ∀ 𝑦 ( 𝑦 = 𝑏 → [ 𝑎 / 𝑥 ] 𝜓 ) )
19		vex	⊢ 𝑏 ∈ V
20	19	sbc6	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑏 → [ 𝑎 / 𝑥 ] 𝜓 ) )
21	18 20	sylibr	⊢ ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) → [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )
22	21	exlimiv	⊢ ( ∃ 𝑝 ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝜑 ) → [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )
23	2 22	sylbi	⊢ ( [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 → [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )
24		sbc5	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = 𝑏 ∧ [ 𝑎 / 𝑥 ] 𝜓 ) )
25		sbc5	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ ∃ 𝑥 ( 𝑥 = 𝑎 ∧ 𝜓 ) )
26	1	bicomd	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜓 ↔ 𝜑 ) )
27	6 26	syl	⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝜓 ↔ 𝜑 ) )
28	27	biimpd	⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝜓 → 𝜑 ) )
29	28	expcom	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜓 → 𝜑 ) ) )
30	29	com13	⊢ ( 𝜓 → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) ) )
31	30	expd	⊢ ( 𝜓 → ( 𝑥 = 𝑎 → ( 𝑦 = 𝑏 → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) ) ) )
32	31	impcom	⊢ ( ( 𝑥 = 𝑎 ∧ 𝜓 ) → ( 𝑦 = 𝑏 → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) ) )
33	32	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑎 ∧ 𝜓 ) → ( 𝑦 = 𝑏 → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) ) )
34	25 33	sylbi	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 → ( 𝑦 = 𝑏 → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) ) )
35	34	impcom	⊢ ( ( 𝑦 = 𝑏 ∧ [ 𝑎 / 𝑥 ] 𝜓 ) → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) )
36	35	exlimiv	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑏 ∧ [ 𝑎 / 𝑥 ] 𝜓 ) → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) )
37	24 36	sylbi	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 → ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) )
38	37	alrimiv	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 → ∀ 𝑝 ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) )
39		prex	⊢ { 𝑎 , 𝑏 } ∈ V
40	39	sbc6	⊢ ( [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 ↔ ∀ 𝑝 ( 𝑝 = { 𝑎 , 𝑏 } → 𝜑 ) )
41	38 40	sylibr	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 → [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 )
42	23 41	impbii	⊢ ( [ { 𝑎 , 𝑏 } / 𝑝 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 )