w-bnj15 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > w-bnj15		Structured version Visualization version GIF version

Syntax Definition w-bnj15 32680

Description: Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.)

**Hypotheses**
Ref	Expression
cA	class 𝐴
cR	class 𝑅

**Assertion**
Ref	Expression
w-bnj15	wff 𝑅 FrSe 𝐴

See definition df-bnj15 32681 for more information.

Colors of variables: wff setvar class