Metamath Proof Explorer


Theorem bj-sngleq

Description: Substitution property for sngl . (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-sngleq ( 𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵 )

Proof

Step Hyp Ref Expression
1 rexeq ( 𝐴 = 𝐵 → ( ∃ 𝑦𝐴 𝑥 = { 𝑦 } ↔ ∃ 𝑦𝐵 𝑥 = { 𝑦 } ) )
2 1 abbidv ( 𝐴 = 𝐵 → { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = { 𝑦 } } = { 𝑥 ∣ ∃ 𝑦𝐵 𝑥 = { 𝑦 } } )
3 df-bj-sngl sngl 𝐴 = { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = { 𝑦 } }
4 df-bj-sngl sngl 𝐵 = { 𝑥 ∣ ∃ 𝑦𝐵 𝑥 = { 𝑦 } }
5 2 3 4 3eqtr4g ( 𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵 )