Theorem csboprabg 34053

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 4274	. . 3 ⊢ ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ [𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
2		sbcex2 3739	. . . . 5 ⊢ ([𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦[𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
3		sbcex2 3739	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧[𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
4		sbcex2 3739	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑[𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑))
5		sbcan 3727	. . . . . . . . . . 11 ⊢ ([𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑))
6		sbcg 3752	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ↔ 𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩))
7	6	anbi1d 620	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑) ↔ (𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
8	5, 7	syl5bb 275	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ (𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
9	8	exbidv 1880	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (∃𝑑[𝐴 / 𝑥](𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
10	4, 9	syl5bb 275	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
11	10	exbidv 1880	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (∃𝑧[𝐴 / 𝑥]∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
12	3, 11	syl5bb 275	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
13	12	exbidv 1880	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦[𝐴 / 𝑥]∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
14	2, 13	syl5bb 275	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)))
15	14	abbidv 2843	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑐 ∣ [𝐴 / 𝑥]∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)})
16	1, 15	syl5eq 2826	. 2 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)})
17		df-oprab 6982	. . 3 ⊢ {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
18	17	csbeq2i 4258	. 2 ⊢ ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = ⦋𝐴 / 𝑥⦌{𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ 𝜑)}
19		df-oprab 6982	. 2 ⊢ {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑} = {𝑐 ∣ ∃𝑦∃𝑧∃𝑑(𝑐 = ⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∧ [𝐴 / 𝑥]𝜑)}
20	16, 18, 19	3eqtr4g 2839	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507  ∃wex 1742   ∈ wcel 2050  {cab 2758  [wsbc 3683  ⦋csb 3788  ⟨cop 4448  {coprab 6979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-nul 4181  df-oprab 6982

This theorem is referenced by:  csbmpo123  34054