Metamath Proof Explorer


Theorem rabbiiaOLD

Description: Obsolete version of rabbiia as of 12-Jan-2025. (Contributed by NM, 22-May-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabbiia.1 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
Assertion rabbiiaOLD { 𝑥𝐴𝜑 } = { 𝑥𝐴𝜓 }

Proof

Step Hyp Ref Expression
1 rabbiia.1 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
2 1 pm5.32i ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐴𝜓 ) )
3 2 abbii { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑥 ∣ ( 𝑥𝐴𝜓 ) }
4 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
5 df-rab { 𝑥𝐴𝜓 } = { 𝑥 ∣ ( 𝑥𝐴𝜓 ) }
6 3 4 5 3eqtr4i { 𝑥𝐴𝜑 } = { 𝑥𝐴𝜓 }