Description: Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | disjdmqseqeq1 | |- ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjeq | |- ( R = S -> ( Disj R <-> Disj S ) ) |
|
2 | dmqseqeq1 | |- ( R = S -> ( ( dom R /. R ) = A <-> ( dom S /. S ) = A ) ) |
|
3 | 1 2 | anbi12d | |- ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) ) |