Theorem rabrabi 3440

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2142 and ax-11 2158. (Revised by Gino Giotto, 20-Aug-2023.)

Hypothesis

Ref	Expression
rabrabi.1	⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))

Assertion

Ref	Expression
rabrabi	⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)}

Distinct variable groups:   𝑥,𝐴,𝑦   𝜑,𝑥   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑥)

Proof of Theorem rabrabi

Step	Hyp	Ref	Expression
1		rabrabi.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))
2	1	cbvrabv 3439	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜒} = {𝑦 ∈ 𝐴 ∣ 𝜑}
3	2	rabeqi 3429	. 2 ⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜒} ∣ 𝜓} = {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓}
4		rabrab 3332	. 2 ⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜒} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)}
5	3, 4	eqtr3i 2823	1 ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)}

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  wlksnwwlknvbij  27694