**Description:** Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Mario
Carneiro, 13-Oct-2016)

Ref | Expression | ||
---|---|---|---|

Hypotheses | csbied.1 | $${\u22a2}{\phi}\to {A}\in {V}$$ | |

csbied.2 | $${\u22a2}\left({\phi}\wedge {x}={A}\right)\to {B}={C}$$ | ||

Assertion | csbied | $${\u22a2}{\phi}\to \u298b{A}/{x}\u298c{B}={C}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | csbied.1 | $${\u22a2}{\phi}\to {A}\in {V}$$ | |

2 | csbied.2 | $${\u22a2}\left({\phi}\wedge {x}={A}\right)\to {B}={C}$$ | |

3 | nfv | $${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$ | |

4 | nfcvd | $${\u22a2}{\phi}\to \underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{C}$$ | |

5 | 3 4 1 2 | csbiedf | $${\u22a2}{\phi}\to \u298b{A}/{x}\u298c{B}={C}$$ |