Description: Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Feb-2005) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 20-Sep-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sb5rf.1 | |- F/ y ph |
|
| Assertion | sb5rf | |- ( ph <-> E. y ( y = x /\ [ y / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb5rf.1 | |- F/ y ph |
|
| 2 | sbequ12r | |- ( y = x -> ( [ y / x ] ph <-> ph ) ) |
|
| 3 | 1 2 | equsex | |- ( E. y ( y = x /\ [ y / x ] ph ) <-> ph ) |
| 4 | 3 | bicomi | |- ( ph <-> E. y ( y = x /\ [ y / x ] ph ) ) |