Metamath Proof Explorer


Theorem bnj1454

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

Ref Expression
Hypothesis bnj1454.1 𝐴 = { 𝑥𝜑 }
Assertion bnj1454 ( 𝐵 ∈ V → ( 𝐵𝐴[ 𝐵 / 𝑥 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 bnj1454.1 𝐴 = { 𝑥𝜑 }
2 1 eleq2i ( 𝐵𝐴𝐵 ∈ { 𝑥𝜑 } )
3 df-sbc ( [ 𝐵 / 𝑥 ] 𝜑𝐵 ∈ { 𝑥𝜑 } )
4 3 a1i ( 𝐵 ∈ V → ( [ 𝐵 / 𝑥 ] 𝜑𝐵 ∈ { 𝑥𝜑 } ) )
5 2 4 bitr4id ( 𝐵 ∈ V → ( 𝐵𝐴[ 𝐵 / 𝑥 ] 𝜑 ) )