Metamath Proof Explorer


Theorem rabeqcOLD

Description: Obsolete version of rabeqc as of 15-Jan-2025. (Contributed by AV, 20-Apr-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabeqcOLD.1
|- ( x e. A -> ph )
Assertion rabeqcOLD
|- { x e. A | ph } = A

Proof

Step Hyp Ref Expression
1 rabeqcOLD.1
 |-  ( x e. A -> ph )
2 df-rab
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
3 eqabcb
 |-  ( { x | ( x e. A /\ ph ) } = A <-> A. x ( ( x e. A /\ ph ) <-> x e. A ) )
4 1 pm4.71i
 |-  ( x e. A <-> ( x e. A /\ ph ) )
5 4 bicomi
 |-  ( ( x e. A /\ ph ) <-> x e. A )
6 3 5 mpgbir
 |-  { x | ( x e. A /\ ph ) } = A
7 2 6 eqtri
 |-  { x e. A | ph } = A