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 ( ∀ 𝑥𝐴 𝜑𝐴 = { 𝑥𝐴𝜑 } )

Proof

Step Hyp Ref Expression
1 pm4.71 ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐴 ↔ ( 𝑥𝐴𝜑 ) ) )
2 1 albii ( ∀ 𝑥 ( 𝑥𝐴𝜑 ) ↔ ∀ 𝑥 ( 𝑥𝐴 ↔ ( 𝑥𝐴𝜑 ) ) )
3 eqab ( ∀ 𝑥 ( 𝑥𝐴 ↔ ( 𝑥𝐴𝜑 ) ) → 𝐴 = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
4 2 3 sylbi ( ∀ 𝑥 ( 𝑥𝐴𝜑 ) → 𝐴 = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
5 df-ral ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥𝐴𝜑 ) )
6 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
7 6 eqeq2i ( 𝐴 = { 𝑥𝐴𝜑 } ↔ 𝐴 = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
8 4 5 7 3imtr4i ( ∀ 𝑥𝐴 𝜑𝐴 = { 𝑥𝐴𝜑 } )