Description: An alternate definition of proper substitution df-sb that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 6-Mar-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfsb3 | |- ( [ y / x ] ph <-> ( ( x = y -> -. ph ) -> A. x ( x = y -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-or | |- ( ( ( x = y /\ ph ) \/ A. x ( x = y -> ph ) ) <-> ( -. ( x = y /\ ph ) -> A. x ( x = y -> ph ) ) ) |
|
| 2 | dfsb2 | |- ( [ y / x ] ph <-> ( ( x = y /\ ph ) \/ A. x ( x = y -> ph ) ) ) |
|
| 3 | imnan | |- ( ( x = y -> -. ph ) <-> -. ( x = y /\ ph ) ) |
|
| 4 | 3 | imbi1i | |- ( ( ( x = y -> -. ph ) -> A. x ( x = y -> ph ) ) <-> ( -. ( x = y /\ ph ) -> A. x ( x = y -> ph ) ) ) |
| 5 | 1 2 4 | 3bitr4i | |- ( [ y / x ] ph <-> ( ( x = y -> -. ph ) -> A. x ( x = y -> ph ) ) ) |