Theorem isf34lem2

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
Assertion	isf34lem2	$$⊢A\in V\to F:𝒫A⟶𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2		difss	$$⊢A\setminus x\subseteq A$$
3		elpw2g	$$⊢A\in V\to \left(A\setminus x\in 𝒫A\leftrightarrow A\setminus x\subseteq A\right)$$
4	2 3	mpbiri	$$⊢A\in V\to A\setminus x\in 𝒫A$$
5	4	adantr	$$⊢\left(A\in V\wedge x\in 𝒫A\right)\to A\setminus x\in 𝒫A$$
6	5 1	fmptd	$$⊢A\in V\to F:𝒫A⟶𝒫A$$