Theorem vtocl 2740

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 1508	. 2 ⊢ Ⅎ𝑥𝜓
2		vtocl.1	. 2 ⊢ 𝐴 ∈ V
3		vtocl.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtocl.3	. 2 ⊢ 𝜑
5	1, 2, 3, 4	vtoclf 2739	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  Vcvv 2686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  vtoclb  2743  zfauscl  4048  bnd2  4097  uniex  4359  ordtriexmid  4437  onsucsssucexmid  4442  regexmid  4450  ordsoexmid  4477  onintexmid  4487  reg3exmid  4494  nnregexmid  4534  acexmidlemv  5772  caovcan  5935  findcard2  6783  findcard2s  6784  inffiexmid  6800  sup3exmid  8715  bj-uniex  13115  bj-omtrans  13154