Theorem csboprabg

Description: Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csboprabg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
2		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
3		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
4		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
5		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
6		sbcg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ↔ 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ) )
7	6	anbi1d	⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
8	5 7	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
9	8	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑑 [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
10	4 9	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
11	10	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑧 [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
12	3 11	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
13	12	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
14	2 13	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
15	14	abbidv	⊢ ( 𝐴 ∈ 𝑉 → { 𝑐 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) } )
16	1 15	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) } )
17		df-oprab	⊢ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
18	17	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
19		df-oprab	⊢ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) }
20	16 18 19	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )