Metamath Proof Explorer


Theorem scotteqd

Description: Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023)

Ref Expression
Hypothesis scotteqd.1 ( 𝜑𝐴 = 𝐵 )
Assertion scotteqd ( 𝜑 → Scott 𝐴 = Scott 𝐵 )

Proof

Step Hyp Ref Expression
1 scotteqd.1 ( 𝜑𝐴 = 𝐵 )
2 1 adantr ( ( 𝜑𝑥𝐴 ) → 𝐴 = 𝐵 )
3 2 raleqdv ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑦𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦𝐵 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
4 1 3 rabeqbidva ( 𝜑 → { 𝑥𝐴 ∣ ∀ 𝑦𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥𝐵 ∣ ∀ 𝑦𝐵 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
5 df-scott Scott 𝐴 = { 𝑥𝐴 ∣ ∀ 𝑦𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
6 df-scott Scott 𝐵 = { 𝑥𝐵 ∣ ∀ 𝑦𝐵 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
7 4 5 6 3eqtr4g ( 𝜑 → Scott 𝐴 = Scott 𝐵 )