# Metamath Proof Explorer

## Theorem elrab

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)

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

### Proof

Step Hyp Ref Expression
1 elrab.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 elex ${⊢}{A}\in \left\{{x}\in {B}|{\phi }\right\}\to {A}\in \mathrm{V}$
3 elex ${⊢}{A}\in {B}\to {A}\in \mathrm{V}$
4 3 adantr ${⊢}\left({A}\in {B}\wedge {\psi }\right)\to {A}\in \mathrm{V}$
5 eleq1 ${⊢}{x}={A}\to \left({x}\in {B}↔{A}\in {B}\right)$
6 5 1 anbi12d ${⊢}{x}={A}\to \left(\left({x}\in {B}\wedge {\phi }\right)↔\left({A}\in {B}\wedge {\psi }\right)\right)$
7 df-rab ${⊢}\left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
8 6 7 elab2g ${⊢}{A}\in \mathrm{V}\to \left({A}\in \left\{{x}\in {B}|{\phi }\right\}↔\left({A}\in {B}\wedge {\psi }\right)\right)$
9 2 4 8 pm5.21nii ${⊢}{A}\in \left\{{x}\in {B}|{\phi }\right\}↔\left({A}\in {B}\wedge {\psi }\right)$