Theorem vtoclg 2590

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)

Hypotheses

Ref	Expression
vtoclg.1	⊢ (x = A → (φ ↔ ψ))
vtoclg.2	⊢ φ

Assertion

Ref	Expression
vtoclg	⊢ (A ∈ 𝑉 → ψ)

Distinct variable groups:   x,A   ψ,x

Allowed substitution hints:   φ(x)   𝑉(x)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		nfcv 2160	. 2 ⊢ ℲxA
2		nfv 1402	. 2 ⊢ Ⅎxψ
3		vtoclg.1	. 2 ⊢ (x = A → (φ ↔ ψ))
4		vtoclg.2	. 2 ⊢ φ
5	1, 2, 3, 4	vtoclgf 2589	1 ⊢ (A ∈ 𝑉 → ψ)

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1228   ∈ wcel 1374

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537

This theorem is referenced by:  vtoclbg  2591  ceqex  2648  mo2icl  2697  nelrdva  2723  sbctt  2801  sbcnestgf  2874  csbing  3121  prnzg  3466  sneqrg  3507  unisng  3571  csbopabg  3809  trss  3837  inex1g  3867  ssexg  3870  pwexg  3907  prexgOLD  3920  prexg  3921  opth  3948  ordelord  4067  uniexg  4125  vtoclr  4315  resieq  4549  csbima12g  4613  dmsnsnsng  4725  iota5  4814  csbiotag  4822  funmo  4843  fconstg  5008  funfveu  5113  funbrfv  5137  fnbrfvb  5139  fvelimab  5154  ssimaexg  5160  fvelrn  5223  isoselem  5384  csbriotag  5404  csbov123g  5466  ovg  5562  tfrexlem  5870  prcdnql  6338  prcunqu  6339  prdisj  6346  bdzfauscl  7263  bdinex1g  7271  bdssexg  7274  bj-prexg  7281  bj-uniexg  7288