# Metamath Proof Explorer

## Theorem vtocl2g

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995) Remove dependency on ax-10 , ax-11 , and ax-13 . (Revised by Steven Nguyen, 29-Nov-2022)

Ref Expression
Hypotheses vtocl2g.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
vtocl2g.2 ${⊢}{y}={B}\to \left({\psi }↔{\chi }\right)$
vtocl2g.3 ${⊢}{\phi }$
Assertion vtocl2g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {\chi }$

### Proof

Step Hyp Ref Expression
1 vtocl2g.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 vtocl2g.2 ${⊢}{y}={B}\to \left({\psi }↔{\chi }\right)$
3 vtocl2g.3 ${⊢}{\phi }$
4 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
5 2 imbi2d ${⊢}{y}={B}\to \left(\left({A}\in \mathrm{V}\to {\psi }\right)↔\left({A}\in \mathrm{V}\to {\chi }\right)\right)$
6 1 3 vtoclg ${⊢}{A}\in \mathrm{V}\to {\psi }$
7 5 6 vtoclg ${⊢}{B}\in {W}\to \left({A}\in \mathrm{V}\to {\chi }\right)$
8 4 7 mpan9 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {\chi }$