Theorem sbcop1

Description: The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023)

	Ref	Expression
Hypothesis	sbcop.z	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	sbcop1	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcop.z	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		sbc5	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ ∃ 𝑥 ( 𝑥 = 𝑎 ∧ 𝜓 ) )
3		opeq1	⊢ ( 𝑎 = 𝑥 → ⟨ 𝑎 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
4	3	equcoms	⊢ ( 𝑥 = 𝑎 → ⟨ 𝑎 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
5	4	eqeq2d	⊢ ( 𝑥 = 𝑎 → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6	1	biimprd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 → 𝜑 ) )
7	5 6	syl6bi	⊢ ( 𝑥 = 𝑎 → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → ( 𝜓 → 𝜑 ) ) )
8	7	com23	⊢ ( 𝑥 = 𝑎 → ( 𝜓 → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) ) )
9	8	imp	⊢ ( ( 𝑥 = 𝑎 ∧ 𝜓 ) → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) )
10	9	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑎 ∧ 𝜓 ) → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) )
11	2 10	sylbi	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) )
12	11	alrimiv	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 → ∀ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) )
13		opex	⊢ ⟨ 𝑎 , 𝑦 ⟩ ∈ V
14	13	sbc6	⊢ ( [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ ∀ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → 𝜑 ) )
15	12 14	sylibr	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 → [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )
16		sbc5	⊢ ( [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ∧ 𝜑 ) )
17	1	biimpd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 → 𝜓 ) )
18	5 17	syl6bi	⊢ ( 𝑥 = 𝑎 → ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → ( 𝜑 → 𝜓 ) ) )
19	18	com3l	⊢ ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ → ( 𝜑 → ( 𝑥 = 𝑎 → 𝜓 ) ) )
20	19	imp	⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ∧ 𝜑 ) → ( 𝑥 = 𝑎 → 𝜓 ) )
21	20	alrimiv	⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑎 → 𝜓 ) )
22		vex	⊢ 𝑎 ∈ V
23	22	sbc6	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ ∀ 𝑥 ( 𝑥 = 𝑎 → 𝜓 ) )
24	21 23	sylibr	⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ∧ 𝜑 ) → [ 𝑎 / 𝑥 ] 𝜓 )
25	24	exlimiv	⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑦 ⟩ ∧ 𝜑 ) → [ 𝑎 / 𝑥 ] 𝜓 )
26	16 25	sylbi	⊢ ( [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 → [ 𝑎 / 𝑥 ] 𝜓 )
27	15 26	impbii	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )