Theorem csboprabg 36814

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

Assertion

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

Distinct variable groups:   𝐴,𝑑   𝑦,𝐴   𝑧,𝐴   𝑉,𝑑   𝑦,𝑉   𝑧,𝑉   𝑥,𝑑   𝑥,𝑦   𝑥,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑑)   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem csboprabg

Dummy variable 𝑐 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098  {cab 2704  [wsbc 3776  ⦋csb 3892  ⟨cop 4636  {coprab 7425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-nul 4325  df-oprab 7428

This theorem is referenced by:  csbmpo123  36815