Metamath Proof Explorer


Theorem scotteqd

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

Ref Expression
Hypothesis scotteqd.1 φ A = B
Assertion scotteqd φ Scott A = Scott B

Proof

Step Hyp Ref Expression
1 scotteqd.1 φ A = B
2 1 adantr φ x A A = B
3 2 raleqdv φ x A y A rank x rank y y B rank x rank y
4 1 3 rabeqbidva φ x A | y A rank x rank y = x B | y B rank x rank y
5 df-scott Scott A = x A | y A rank x rank y
6 df-scott Scott B = x B | y B rank x rank y
7 4 5 6 3eqtr4g φ Scott A = Scott B