Theorem isfildlem

Description: Lemma for isfild . (Contributed by Mario Carneiro, 1-Dec-2013)

	Ref	Expression
Hypotheses	isfild.1	$$⊢\phi \to \left(x\in F\leftrightarrow \left(x\subseteq A\wedge \psi \right)\right)$$
	isfild.2	$$⊢\phi \to A\in V$$
Assertion	isfildlem	$$⊢\phi \to \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfild.1	$$⊢\phi \to \left(x\in F\leftrightarrow \left(x\subseteq A\wedge \psi \right)\right)$$
2		isfild.2	$$⊢\phi \to A\in V$$
3		elex	$$⊢B\in F\to B\in \mathrm{V}$$
4	3	a1i	$$⊢\phi \to \left(B\in F\to B\in \mathrm{V}\right)$$
5		ssexg	$$⊢\left(B\subseteq A\wedge A\in V\right)\to B\in \mathrm{V}$$
6	5	expcom	$$⊢A\in V\to \left(B\subseteq A\to B\in \mathrm{V}\right)$$
7	2 6	syl	$$⊢\phi \to \left(B\subseteq A\to B\in \mathrm{V}\right)$$
8	7	adantrd	$$⊢\phi \to \left(\left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\to B\in \mathrm{V}\right)$$
9		eleq1	$$⊢y=B\to \left(y\in F\leftrightarrow B\in F\right)$$
10		sseq1	$$⊢y=B\to \left(y\subseteq A\leftrightarrow B\subseteq A\right)$$
11		dfsbcq	$$⊢y=B\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)$$
12	10 11	anbi12d	$$⊢y=B\to \left(\left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)$$
13	9 12	bibi12d	$$⊢y=B\to \left(\left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)\leftrightarrow \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
14	13	imbi2d	$$⊢y=B\to \left(\left(\phi \to \left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)\right)\leftrightarrow \left(\phi \to \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)\right)\right)$$
15		nfv	$$⊢Ⅎx\phi$$
16		nfv	$$⊢Ⅎxy\in F$$
17		nfv	$$⊢Ⅎxy\subseteq A$$
18		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi$$
19	17 18	nfan	$$⊢Ⅎx\left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
20	16 19	nfbi	$$⊢Ⅎx\left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)$$
21	15 20	nfim	$$⊢Ⅎx\left(\phi \to \left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
22		eleq1	$$⊢x=y\to \left(x\in F\leftrightarrow y\in F\right)$$
23		sseq1	$$⊢x=y\to \left(x\subseteq A\leftrightarrow y\subseteq A\right)$$
24		sbceq1a	$$⊢x=y\to \left(\psi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
25	23 24	anbi12d	$$⊢x=y\to \left(\left(x\subseteq A\wedge \psi \right)\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)$$
26	22 25	bibi12d	$$⊢x=y\to \left(\left(x\in F\leftrightarrow \left(x\subseteq A\wedge \psi \right)\right)\leftrightarrow \left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
27	26	imbi2d	$$⊢x=y\to \left(\left(\phi \to \left(x\in F\leftrightarrow \left(x\subseteq A\wedge \psi \right)\right)\right)\leftrightarrow \left(\phi \to \left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)\right)\right)$$
28	21 27 1	chvarfv	$$⊢\phi \to \left(y\in F\leftrightarrow \left(y\subseteq A\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)$$
29	14 28	vtoclg	$$⊢B\in \mathrm{V}\to \left(\phi \to \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
30	29	com12	$$⊢\phi \to \left(B\in \mathrm{V}\to \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
31	4 8 30	pm5.21ndd	$$⊢\phi \to \left(B\in F\leftrightarrow \left(B\subseteq A\wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\psi \right)\right)$$