Theorem abfmpel

Description: Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016)

	Ref	Expression
Hypotheses	abfmpel.1	$$⊢F=\left(x\in V⟼\left\{y|\phi \right\}\right)$$
	abfmpel.2	$$⊢\left\{y|\phi \right\}\in \mathrm{V}$$
	abfmpel.3	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	abfmpel	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in F\left(A\right)\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abfmpel.1	$$⊢F=\left(x\in V⟼\left\{y|\phi \right\}\right)$$
2		abfmpel.2	$$⊢\left\{y|\phi \right\}\in \mathrm{V}$$
3		abfmpel.3	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
4	2	csbex	$$⊢⦋A/x⦌\left\{y|\phi \right\}\in \mathrm{V}$$
5	1	fvmpts	$$⊢\left(A\in V\wedge ⦋A/x⦌\left\{y|\phi \right\}\in \mathrm{V}\right)\to F\left(A\right)=⦋A/x⦌\left\{y|\phi \right\}$$
6	4 5	mpan2	$$⊢A\in V\to F\left(A\right)=⦋A/x⦌\left\{y|\phi \right\}$$
7		csbab	$$⊢⦋A/x⦌\left\{y|\phi \right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$
8	6 7	eqtrdi	$$⊢A\in V\to F\left(A\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$
9	8	eleq2d	$$⊢A\in V\to \left(B\in F\left(A\right)\leftrightarrow B\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\right)$$
10	9	adantr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in F\left(A\right)\leftrightarrow B\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\right)$$
11		simpl	$$⊢\left(A\in V\wedge y=B\right)\to A\in V$$
12	3	ancoms	$$⊢\left(y=B\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
13	12	adantll	$$⊢\left(\left(A\in V\wedge y=B\right)\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
14	11 13	sbcied	$$⊢\left(A\in V\wedge y=B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
15	14	ex	$$⊢A\in V\to \left(y=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
16	15	alrimiv	$$⊢A\in V\to \forall y\left(y=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)$$
17		elabgt	$$⊢\left(B\in W\wedge \forall y\left(y=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)\right)\right)\to \left(B\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\leftrightarrow \psi \right)$$
18	16 17	sylan2	$$⊢\left(B\in W\wedge A\in V\right)\to \left(B\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\leftrightarrow \psi \right)$$
19	18	ancoms	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\leftrightarrow \psi \right)$$
20	10 19	bitrd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\in F\left(A\right)\leftrightarrow \psi \right)$$