Theorem bnj976

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj976.1	⊢ ( 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
	bnj976.2	⊢ ( 𝜑′ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
	bnj976.3	⊢ ( 𝜓′ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
	bnj976.4	⊢ ( 𝜒′ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
	bnj976.5	⊢ 𝐺 ∈ V
Assertion	bnj976	⊢ ( 𝜒′ ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )

Proof

Step	Hyp	Ref	Expression
1		bnj976.1	⊢ ( 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
2		bnj976.2	⊢ ( 𝜑′ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
3		bnj976.3	⊢ ( 𝜓′ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
4		bnj976.4	⊢ ( 𝜒′ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
5		bnj976.5	⊢ 𝐺 ∈ V
6		sbccow	⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ [ 𝐺 / 𝑓 ] 𝜒 )
7		bnj252	⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
8	7	sbcbii	⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
9	1	sbcbii	⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
10		vex	⊢ ℎ ∈ V
11	10	bnj525	⊢ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ↔ 𝑁 ∈ 𝐷 )
12		sbc3an	⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
13		bnj62	⊢ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ↔ ℎ Fn 𝑁 )
14	13	3anbi1i	⊢ ( ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
15	12 14	bitri	⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
16	11 15	anbi12i	⊢ ( ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) )
17		sbcan	⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
18		bnj252	⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) )
19	16 17 18	3bitr4ri	⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
20	8 9 19	3bitr4i	⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
21		fneq1	⊢ ( ℎ = 𝐺 → ( ℎ Fn 𝑁 ↔ 𝐺 Fn 𝑁 ) )
22		sbceq1a	⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ) )
23		sbccow	⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / 𝑓 ] 𝜑 )
24	2 23	bitr4i	⊢ ( 𝜑′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 )
25	22 24	bitr4di	⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ 𝜑′ ) )
26		sbceq1a	⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ) )
27		sbccow	⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] 𝜓 )
28	3 27	bitr4i	⊢ ( 𝜓′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 )
29	26 28	bitr4di	⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ 𝜓′ ) )
30	21 25 29	3anbi123d	⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
31	30	anbi2d	⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) )
32		bnj252	⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
33	31 18 32	3bitr4g	⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
34	20 33	bitrid	⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
35	5 34	sbcie	⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )
36	4 6 35	3bitr2i	⊢ ( 𝜒′ ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )