Theorem csboprabg 36211

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 4438	. . 3 ⊢ ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ [𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
2		sbcex2 3843	. . . . 5 ⊢ ([𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦[𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
3		sbcex2 3843	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧[𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
4		sbcex2 3843	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑[𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
5		sbcan 3830	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑))
6		sbcg 3857	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ↔ 𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩))
7	6	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑) ↔ (𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
8	5, 7	bitrid 283	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ (𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
9	8	exbidv 1925	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (∃𝑑[𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
10	4, 9	bitrid 283	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
11	10	exbidv 1925	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (∃𝑧[𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
12	3, 11	bitrid 283	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
13	12	exbidv 1925	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦[𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
14	2, 13	bitrid 283	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
15	14	abbidv 2802	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑐 ∣ [𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)})
16	1, 15	eqtrid 2785	. 2 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)})
17		df-oprab 7413	. . 3 ⊢ {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
18	17	csbeq2i 3902	. 2 ⊢ ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
19		df-oprab 7413	. 2 ⊢ {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)}
20	16, 18, 19	3eqtr4g 2798	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  [wsbc 3778  ⦋csb 3894  ⟨cop 4635  {coprab 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-nul 4324  df-oprab 7413

This theorem is referenced by:  csbmpo123  36212