# Metamath Proof Explorer

## Theorem rabrabi

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

Ref Expression
Hypothesis rabrabi.1 ${⊢}{x}={y}\to \left({\chi }↔{\phi }\right)$
Assertion rabrabi ${⊢}\left\{{x}\in \left\{{y}\in {A}|{\phi }\right\}|{\psi }\right\}=\left\{{x}\in {A}|\left({\chi }\wedge {\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 rabrabi.1 ${⊢}{x}={y}\to \left({\chi }↔{\phi }\right)$
2 1 cbvrabv ${⊢}\left\{{x}\in {A}|{\chi }\right\}=\left\{{y}\in {A}|{\phi }\right\}$
3 2 rabeqi ${⊢}\left\{{x}\in \left\{{x}\in {A}|{\chi }\right\}|{\psi }\right\}=\left\{{x}\in \left\{{y}\in {A}|{\phi }\right\}|{\psi }\right\}$
4 rabrab ${⊢}\left\{{x}\in \left\{{x}\in {A}|{\chi }\right\}|{\psi }\right\}=\left\{{x}\in {A}|\left({\chi }\wedge {\psi }\right)\right\}$
5 3 4 eqtr3i ${⊢}\left\{{x}\in \left\{{y}\in {A}|{\phi }\right\}|{\psi }\right\}=\left\{{x}\in {A}|\left({\chi }\wedge {\psi }\right)\right\}$