Theorem isfildlem

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

	Ref	Expression
Hypotheses	isfild.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) )
	isfild.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	isfildlem	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfild.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) )
2		isfild.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		elex	⊢ ( 𝐵 ∈ 𝐹 → 𝐵 ∈ V )
4	3	a1i	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐹 → 𝐵 ∈ V ) )
5		ssexg	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐵 ∈ V )
6	5	expcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ V ) )
7	2 6	syl	⊢ ( 𝜑 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ V ) )
8	7	adantrd	⊢ ( 𝜑 → ( ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) → 𝐵 ∈ V ) )
9		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐹 ↔ 𝐵 ∈ 𝐹 ) )
10		sseq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
11		dfsbcq	⊢ ( 𝑦 = 𝐵 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝐵 / 𝑥 ] 𝜓 ) )
12	10 11	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) )
13	9 12	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) ↔ ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) ) )
14	13	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝜑 → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) ) ) )
15		nfv	⊢ Ⅎ 𝑥 𝜑
16		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐹
17		nfv	⊢ Ⅎ 𝑥 𝑦 ⊆ 𝐴
18		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜓
19	17 18	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 )
20	16 19	nfbi	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
21	15 20	nfim	⊢ Ⅎ 𝑥 ( 𝜑 → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
22		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐹 ↔ 𝑦 ∈ 𝐹 ) )
23		sseq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
24		sbceq1a	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )
25	23 24	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
26	22 25	bibi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) ) )
27	26	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) ) ) )
28	21 27 1	chvarfv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐹 ↔ ( 𝑦 ⊆ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
29	14 28	vtoclg	⊢ ( 𝐵 ∈ V → ( 𝜑 → ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) ) )
30	29	com12	⊢ ( 𝜑 → ( 𝐵 ∈ V → ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) ) )
31	4 8 30	pm5.21ndd	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐹 ↔ ( 𝐵 ⊆ 𝐴 ∧ [ 𝐵 / 𝑥 ] 𝜓 ) ) )