Theorem freq2

Description: Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994)

	Ref	Expression
Assertion	freq2	$$⊢A=B\to \left(R\mathrm{Fr}A\leftrightarrow R\mathrm{Fr}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2		frss	$$⊢B\subseteq A\to \left(R\mathrm{Fr}A\to R\mathrm{Fr}B\right)$$
3	1 2	syl	$$⊢A=B\to \left(R\mathrm{Fr}A\to R\mathrm{Fr}B\right)$$
4		eqimss	$$⊢A=B\to A\subseteq B$$
5		frss	$$⊢A\subseteq B\to \left(R\mathrm{Fr}B\to R\mathrm{Fr}A\right)$$
6	4 5	syl	$$⊢A=B\to \left(R\mathrm{Fr}B\to R\mathrm{Fr}A\right)$$
7	3 6	impbid	$$⊢A=B\to \left(R\mathrm{Fr}A\leftrightarrow R\mathrm{Fr}B\right)$$