This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993)
|
|
Ref |
Expression |
|
Hypotheses |
vtoclef.1 |
|- F/ x ph |
|
|
vtoclef.2 |
|- A e. _V |
|
|
vtoclef.3 |
|- ( x = A -> ph ) |
|
Assertion |
vtoclef |
|- ph |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
vtoclef.1 |
|- F/ x ph |
| 2 |
|
vtoclef.2 |
|- A e. _V |
| 3 |
|
vtoclef.3 |
|- ( x = A -> ph ) |
| 4 |
2
|
isseti |
|- E. x x = A |
| 5 |
1 3
|
exlimi |
|- ( E. x x = A -> ph ) |
| 6 |
4 5
|
ax-mp |
|- ph |