isf34lem1

		Ref	Expression
	Hypothesis	compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
	Assertion	isf34lem1	$⊢ (A \in V \land X \subseteq A) \to F (X) = A ∖ X$

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

Metamath Proof Explorer