Theorem vtoclga 2870

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

Hypotheses

Ref	Expression
vtoclga.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclga.2	⊢ (𝑥 ∈ 𝐵 → 𝜑)

Assertion

Ref	Expression
vtoclga	⊢ (𝐴 ∈ 𝐵 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga

Step	Hyp	Ref	Expression
1		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 2869	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202

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-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  vtoclri  2881  ssuni  3915  ordtriexmid  4619  onsucsssucexmid  4625  tfis3  4684  fvmpt3  5725  fvmptssdm  5731  fnressn  5840  fressnfv  5841  caovord  6194  caovimo  6216  tfrlem1  6474  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnsucsssuc  6660  nntri3or  6661  nnaordi  6676  nnaword  6679  nnmordi  6684  nnaordex  6696  ixpfn  6873  findcard  7077  findcard2  7078  findcard2s  7079  exmidomni  7341  indpi  7562  prarloclem3  7717  uzind4s2  9825  cnref1o  9885  frec2uzrdg  10672  expcl2lemap  10814  seq3coll  11107  climub  11922  climserle  11923  fsum3cvg  11957  summodclem2a  11960  prodfap0  12124  prodfrecap  12125  fproddccvg  12151  alginv  12637  algcvg  12638  algcvga  12641  algfx  12642  prmind2  12710  prmpwdvds  12946  lgsdir2lem4  15779