dfatprc

Description: A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022)

		Ref	Expression
	Assertion	dfatprc	$⊢ \neg A \in V \to \neg F defAt A$

Step	Hyp	Ref	Expression
1		prcnel	$⊢ \neg A \in V \to \neg A \in dom F$
2	1	orcd	$⊢ \neg A \in V \to (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
3		ianor	$⊢ \neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
4		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
5	3 4	xchnxbir	$⊢ \neg F defAt A \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
6	2 5	sylibr	$⊢ \neg A \in V \to \neg F defAt A$

Metamath Proof Explorer