Theorem isf34lem1

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	isf34lem1	$$⊢\left(A\in V\wedge X\subseteq A\right)\to F\left(X\right)=A\setminus X$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2		difeq2	$$⊢x=a\to A\setminus x=A\setminus a$$
3	2	cbvmptv	$$⊢\left(x\in 𝒫A⟼A\setminus x\right)=\left(a\in 𝒫A⟼A\setminus a\right)$$
4	1 3	eqtri	$$⊢F=\left(a\in 𝒫A⟼A\setminus a\right)$$
5		difeq2	$$⊢a=X\to A\setminus a=A\setminus X$$
6		elpw2g	$$⊢A\in V\to \left(X\in 𝒫A\leftrightarrow X\subseteq A\right)$$
7	6	biimpar	$$⊢\left(A\in V\wedge X\subseteq A\right)\to X\in 𝒫A$$
8		difexg	$$⊢A\in V\to A\setminus X\in \mathrm{V}$$
9	8	adantr	$$⊢\left(A\in V\wedge X\subseteq A\right)\to A\setminus X\in \mathrm{V}$$
10	4 5 7 9	fvmptd3	$$⊢\left(A\in V\wedge X\subseteq A\right)\to F\left(X\right)=A\setminus X$$