Theorem vtoclga 2796

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 2312	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1521	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 2795	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141

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-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  vtoclri  2805  ssuni  3816  ordtriexmid  4503  onsucsssucexmid  4509  tfis3  4568  fvmpt3  5573  fvmptssdm  5578  fnressn  5680  fressnfv  5681  caovord  6022  caovimo  6044  tfrlem1  6285  nnacl  6457  nnmcl  6458  nnacom  6461  nnaass  6462  nndi  6463  nnmass  6464  nnmsucr  6465  nnmcom  6466  nnsucsssuc  6469  nntri3or  6470  nnaordi  6485  nnaword  6488  nnmordi  6493  nnaordex  6505  ixpfn  6680  findcard  6864  findcard2  6865  findcard2s  6866  exmidomni  7116  indpi  7297  prarloclem3  7452  uzind4s2  9543  cnref1o  9602  frec2uzrdg  10358  expcl2lemap  10481  seq3coll  10770  climub  11300  climserle  11301  fsum3cvg  11334  summodclem2a  11337  prodfap0  11501  prodfrecap  11502  fproddccvg  11528  alginv  11994  algcvg  11995  algcvga  11998  algfx  11999  prmind2  12067  prmpwdvds  12300  lgsdir2lem4  13691