Theorem elmapintab

Description: Two ways to say a set is an element of mapped intersection of a class. Here F maps elements of C to elements of |^| { x | ph } or x . (Contributed by RP, 19-Aug-2020)

	Ref	Expression
Hypotheses	elmapintab.1	$$⊢A\in B\leftrightarrow \left(A\in C\wedge F\left(A\right)\in \bigcap \left\{x|\phi \right\}\right)$$
	elmapintab.2	$$⊢A\in E\leftrightarrow \left(A\in C\wedge F\left(A\right)\in x\right)$$
Assertion	elmapintab	$$⊢A\in B\leftrightarrow \left(A\in C\wedge \forall x\left(\phi \to A\in E\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmapintab.1	$$⊢A\in B\leftrightarrow \left(A\in C\wedge F\left(A\right)\in \bigcap \left\{x|\phi \right\}\right)$$
2		elmapintab.2	$$⊢A\in E\leftrightarrow \left(A\in C\wedge F\left(A\right)\in x\right)$$
3		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
4	3	elintab	$$⊢F\left(A\right)\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to F\left(A\right)\in x\right)$$
5	4	anbi2i	$$⊢\left(A\in C\wedge F\left(A\right)\in \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in C\wedge \forall x\left(\phi \to F\left(A\right)\in x\right)\right)$$
6	2	baibr	$$⊢A\in C\to \left(F\left(A\right)\in x\leftrightarrow A\in E\right)$$
7	6	imbi2d	$$⊢A\in C\to \left(\left(\phi \to F\left(A\right)\in x\right)\leftrightarrow \left(\phi \to A\in E\right)\right)$$
8	7	albidv	$$⊢A\in C\to \left(\forall x\left(\phi \to F\left(A\right)\in x\right)\leftrightarrow \forall x\left(\phi \to A\in E\right)\right)$$
9	8	pm5.32i	$$⊢\left(A\in C\wedge \forall x\left(\phi \to F\left(A\right)\in x\right)\right)\leftrightarrow \left(A\in C\wedge \forall x\left(\phi \to A\in E\right)\right)$$
10	1 5 9	3bitri	$$⊢A\in B\leftrightarrow \left(A\in C\wedge \forall x\left(\phi \to A\in E\right)\right)$$