Theorem bnj62

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

	Ref	Expression
Assertion	bnj62	⊢ ( [ 𝑧 / 𝑥 ] 𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		fneq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 Fn 𝐴 ↔ 𝑦 Fn 𝐴 ) )
3	1 2	sbcie	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 Fn 𝐴 ↔ 𝑦 Fn 𝐴 )
4	3	sbcbii	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝑥 Fn 𝐴 ↔ [ 𝑧 / 𝑦 ] 𝑦 Fn 𝐴 )
5		sbccow	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝑥 Fn 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑥 Fn 𝐴 )
6		vex	⊢ 𝑧 ∈ V
7		fneq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 Fn 𝐴 ↔ 𝑧 Fn 𝐴 ) )
8	6 7	sbcie	⊢ ( [ 𝑧 / 𝑦 ] 𝑦 Fn 𝐴 ↔ 𝑧 Fn 𝐴 )
9	4 5 8	3bitr3i	⊢ ( [ 𝑧 / 𝑥 ] 𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴 )