Metamath Proof Explorer


Theorem bnj90

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj90.1 𝑌 ∈ V
Assertion bnj90 ( [ 𝑌 / 𝑥 ] 𝑧 Fn 𝑥𝑧 Fn 𝑌 )

Proof

Step Hyp Ref Expression
1 bnj90.1 𝑌 ∈ V
2 fneq2 ( 𝑥 = 𝑦 → ( 𝑧 Fn 𝑥𝑧 Fn 𝑦 ) )
3 fneq2 ( 𝑦 = 𝑌 → ( 𝑧 Fn 𝑦𝑧 Fn 𝑌 ) )
4 2 3 sbcie2g ( 𝑌 ∈ V → ( [ 𝑌 / 𝑥 ] 𝑧 Fn 𝑥𝑧 Fn 𝑌 ) )
5 1 4 ax-mp ( [ 𝑌 / 𝑥 ] 𝑧 Fn 𝑥𝑧 Fn 𝑌 )