Metamath Proof Explorer

Theorem parteq1i

Description: Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Hypothesis parteq1i.1 
|- R = S
Assertion parteq1i 
|- ( R Part A <-> S Part A )

Proof

Step Hyp Ref Expression
1 parteq1i.1 
 |-  R = S
2 parteq1 
 |-  ( R = S -> ( R Part A <-> S Part A ) )
3 1 2 ax-mp 
 |-  ( R Part A <-> S Part A )