Theorem vtocl 2826

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)

Hypotheses

Ref	Expression
vtocl.1	⊢ 𝐴 ∈ V
vtocl.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl.3	⊢ 𝜑

Assertion

Ref	Expression
vtocl	⊢ 𝜓

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtocl

Step	Hyp	Ref	Expression
1		nfv 1550	. 2 ⊢ Ⅎ𝑥𝜓
2		vtocl.1	. 2 ⊢ 𝐴 ∈ V
3		vtocl.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtocl.3	. 2 ⊢ 𝜑
5	1, 2, 3, 4	vtoclf 2825	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   ∈ wcel 2175  Vcvv 2771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  vtoclb  2829  zfauscl  4163  bnd2  4216  uniex  4482  ordtriexmid  4567  onsucsssucexmid  4573  regexmid  4581  ordsoexmid  4608  onintexmid  4619  reg3exmid  4626  nnregexmid  4667  acexmidlemv  5932  caovcan  6101  findcard2  6968  findcard2s  6969  inffiexmid  6985  sup3exmid  9012  bj-uniex  15717  bj-omtrans  15756