Metamath Proof Explorer


Theorem rabid2im

Description: One direction of rabid2 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025)

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

Proof

Step Hyp Ref Expression
1 pm4.71
 |-  ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
2 1 albii
 |-  ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
3 eqab
 |-  ( A. x ( x e. A <-> ( x e. A /\ ph ) ) -> A = { x | ( x e. A /\ ph ) } )
4 2 3 sylbi
 |-  ( A. x ( x e. A -> ph ) -> A = { x | ( x e. A /\ ph ) } )
5 df-ral
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
6 df-rab
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
7 6 eqeq2i
 |-  ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
8 4 5 7 3imtr4i
 |-  ( A. x e. A ph -> A = { x e. A | ph } )