# Metamath Proof Explorer

## Theorem elssabg

Description: Membership in a class abstraction involving a subset. Unlike elabg , A does not have to be a set. (Contributed by NM, 29-Aug-2006)

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

### Proof

Step Hyp Ref Expression
1 elssabg.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 ssexg ${⊢}\left({A}\subseteq {B}\wedge {B}\in {V}\right)\to {A}\in \mathrm{V}$
3 2 expcom ${⊢}{B}\in {V}\to \left({A}\subseteq {B}\to {A}\in \mathrm{V}\right)$
4 3 adantrd ${⊢}{B}\in {V}\to \left(\left({A}\subseteq {B}\wedge {\psi }\right)\to {A}\in \mathrm{V}\right)$
5 sseq1 ${⊢}{x}={A}\to \left({x}\subseteq {B}↔{A}\subseteq {B}\right)$
6 5 1 anbi12d ${⊢}{x}={A}\to \left(\left({x}\subseteq {B}\wedge {\phi }\right)↔\left({A}\subseteq {B}\wedge {\psi }\right)\right)$
7 6 elab3g ${⊢}\left(\left({A}\subseteq {B}\wedge {\psi }\right)\to {A}\in \mathrm{V}\right)\to \left({A}\in \left\{{x}|\left({x}\subseteq {B}\wedge {\phi }\right)\right\}↔\left({A}\subseteq {B}\wedge {\psi }\right)\right)$
8 4 7 syl ${⊢}{B}\in {V}\to \left({A}\in \left\{{x}|\left({x}\subseteq {B}\wedge {\phi }\right)\right\}↔\left({A}\subseteq {B}\wedge {\psi }\right)\right)$