Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj524 Unicode version

Theorem bnj524 29082
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj524.1  |-  ( ph  <->  ps )
bnj524.2  |-  A  e. 
_V
Assertion
Ref Expression
bnj524  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )

Proof of Theorem bnj524
StepHypRef Expression
1 bnj524.2 . 2  |-  A  e. 
_V
2 bnj524.1 . . 3  |-  ( ph  <->  ps )
32sbcbiiOLD 3060 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
41, 3ax-mp 8 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1696   _Vcvv 2801   [.wsbc 3004
This theorem is referenced by:  bnj538  29085  bnj919  29113  bnj91  29209  bnj92  29210  bnj106  29216  bnj121  29218  bnj125  29220  bnj126  29221  bnj130  29222  bnj153  29228  bnj207  29229  bnj523  29235  bnj526  29236  bnj539  29239  bnj540  29240  bnj611  29266  bnj934  29283  bnj1000  29289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator