Metamath Proof Explorer


Theorem rabeqiOLD

Description: Obsolete version of rabeqi as of 3-Jun-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabeqi.1 𝐴 = 𝐵
Assertion rabeqiOLD { 𝑥𝐴𝜑 } = { 𝑥𝐵𝜑 }

Proof

Step Hyp Ref Expression
1 rabeqi.1 𝐴 = 𝐵
2 1 nfth 𝑥 𝐴 = 𝐵
3 eleq2 ( 𝐴 = 𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
4 3 anbi1d ( 𝐴 = 𝐵 → ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐵𝜑 ) ) )
5 2 4 abbid ( 𝐴 = 𝐵 → { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑥 ∣ ( 𝑥𝐵𝜑 ) } )
6 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
7 df-rab { 𝑥𝐵𝜑 } = { 𝑥 ∣ ( 𝑥𝐵𝜑 ) }
8 5 6 7 3eqtr4g ( 𝐴 = 𝐵 → { 𝑥𝐴𝜑 } = { 𝑥𝐵𝜑 } )
9 1 8 ax-mp { 𝑥𝐴𝜑 } = { 𝑥𝐵𝜑 }