Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
rabeqi
Metamath Proof Explorer
Description: Equality theorem for restricted class abstractions. Inference form of
rabeqf . (Contributed by Glauco Siliprandi , 26-Jun-2021) Avoid
ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto , 3-Jun-2024)

Ref
Expression
Hypothesis
rabeqi.1
$${\u22a2}{A}={B}$$
Assertion
rabeqi
$${\u22a2}\left\{{x}\in {A}|{\phi}\right\}=\left\{{x}\in {B}|{\phi}\right\}$$

Proof
Step
Hyp
Ref
Expression
1
rabeqi.1
$${\u22a2}{A}={B}$$
2
1
eleq2i
$${\u22a2}{x}\in {A}\leftrightarrow {x}\in {B}$$
3
2
anbi1i
$${\u22a2}\left({x}\in {A}\wedge {\phi}\right)\leftrightarrow \left({x}\in {B}\wedge {\phi}\right)$$
4
3
rabbia2
$${\u22a2}\left\{{x}\in {A}|{\phi}\right\}=\left\{{x}\in {B}|{\phi}\right\}$$