# Metamath Proof Explorer

## Theorem abbi1

Description: Equivalent formulas yield equal class abstractions (closed form). This is the forward implication of abbi , proved from fewer axioms. (Contributed by BJ and WL and SN, 20-Aug-2023)

Ref Expression
Assertion abbi1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left\{{x}|{\phi }\right\}=\left\{{x}|{\psi }\right\}$

### Proof

Step Hyp Ref Expression
1 spsbbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left(\left[{y}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\psi }\right)$
2 df-clab ${⊢}{y}\in \left\{{x}|{\phi }\right\}↔\left[{y}/{x}\right]{\phi }$
3 df-clab ${⊢}{y}\in \left\{{x}|{\psi }\right\}↔\left[{y}/{x}\right]{\psi }$
4 1 2 3 3bitr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left({y}\in \left\{{x}|{\phi }\right\}↔{y}\in \left\{{x}|{\psi }\right\}\right)$
5 4 eqrdv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left\{{x}|{\phi }\right\}=\left\{{x}|{\psi }\right\}$