ssimaexg

		Ref	Expression
	Assertion	ssimaexg	$⊢ (A \in C \land Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x])$

Step	Hyp	Ref	Expression
1		imaeq2	$⊢ y = A \to F [y] = F [A]$
2	1	sseq2d	$⊢ y = A \to (B \subseteq F [y] \leftrightarrow B \subseteq F [A])$
3	2	anbi2d	$⊢ y = A \to ((Fun F \land B \subseteq F [y]) \leftrightarrow (Fun F \land B \subseteq F [A]))$
4		sseq2	$⊢ y = A \to (x \subseteq y \leftrightarrow x \subseteq A)$
5	4	anbi1d	$⊢ y = A \to ((x \subseteq y \land B = F [x]) \leftrightarrow (x \subseteq A \land B = F [x]))$
6	5	exbidv	$⊢ y = A \to (\exists x (x \subseteq y \land B = F [x]) \leftrightarrow \exists x (x \subseteq A \land B = F [x]))$
7	3 6	imbi12d	$⊢ y = A \to (((Fun F \land B \subseteq F [y]) \to \exists x (x \subseteq y \land B = F [x])) \leftrightarrow ((Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x])))$
8		vex	$⊢ y \in V$
9	8	ssimaex	$⊢ (Fun F \land B \subseteq F [y]) \to \exists x (x \subseteq y \land B = F [x])$
10	7 9	vtoclg	$⊢ A \in C \to ((Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x]))$
11	10	3impib	$⊢ (A \in C \land Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x])$

Metamath Proof Explorer