Theorem bnj873

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj873.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj873.7	⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
	bnj873.8	⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
Assertion	bnj873	⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) }

Proof

Step	Hyp	Ref	Expression
1		bnj873.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
2		bnj873.7	⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
3		bnj873.8	⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
4		nfv	⊢ Ⅎ 𝑔 ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
5		nfcv	⊢ Ⅎ 𝑓 𝐷
6		nfv	⊢ Ⅎ 𝑓 𝑔 Fn 𝑛
7		nfsbc1v	⊢ Ⅎ 𝑓 [ 𝑔 / 𝑓 ] 𝜑
8	2 7	nfxfr	⊢ Ⅎ 𝑓 𝜑′
9		nfsbc1v	⊢ Ⅎ 𝑓 [ 𝑔 / 𝑓 ] 𝜓
10	3 9	nfxfr	⊢ Ⅎ 𝑓 𝜓′
11	6 8 10	nf3an	⊢ Ⅎ 𝑓 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ )
12	5 11	nfrex	⊢ Ⅎ 𝑓 ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ )
13		fneq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝑛 ↔ 𝑔 Fn 𝑛 ) )
14		sbceq1a	⊢ ( 𝑓 = 𝑔 → ( 𝜑 ↔ [ 𝑔 / 𝑓 ] 𝜑 ) )
15	14 2	bitr4di	⊢ ( 𝑓 = 𝑔 → ( 𝜑 ↔ 𝜑′ ) )
16		sbceq1a	⊢ ( 𝑓 = 𝑔 → ( 𝜓 ↔ [ 𝑔 / 𝑓 ] 𝜓 ) )
17	16 3	bitr4di	⊢ ( 𝑓 = 𝑔 → ( 𝜓 ↔ 𝜓′ ) )
18	13 15 17	3anbi123d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) )
19	18	rexbidv	⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) )
20	4 12 19	cbvabw	⊢ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } = { 𝑔 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) }
21	1 20	eqtri	⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) }