Metamath Proof Explorer

Theorem bnj525

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

Ref Expression
Hypothesis bnj525.1 
|- A e. _V
Assertion bnj525 
|- ( [. A / x ]. ph <-> ph )

Proof

Step Hyp Ref Expression
1 bnj525.1 
 |-  A e. _V
2 sbcg 
 |-  ( A e. _V -> ( [. A / x ]. ph <-> ph ) )
3 1 2 ax-mp 
 |-  ( [. A / x ]. ph <-> ph )