Theorem vtoclga 2830

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765

This theorem is referenced by:  vtoclri  2839  ssuni  3861  ordtriexmid  4557  onsucsssucexmid  4563  tfis3  4622  fvmpt3  5640  fvmptssdm  5646  fnressn  5748  fressnfv  5749  caovord  6095  caovimo  6117  tfrlem1  6366  nnacl  6538  nnmcl  6539  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  nnsucsssuc  6550  nntri3or  6551  nnaordi  6566  nnaword  6569  nnmordi  6574  nnaordex  6586  ixpfn  6763  findcard  6949  findcard2  6950  findcard2s  6951  exmidomni  7208  indpi  7409  prarloclem3  7564  uzind4s2  9665  cnref1o  9725  frec2uzrdg  10501  expcl2lemap  10643  seq3coll  10934  climub  11509  climserle  11510  fsum3cvg  11543  summodclem2a  11546  prodfap0  11710  prodfrecap  11711  fproddccvg  11737  alginv  12215  algcvg  12216  algcvga  12219  algfx  12220  prmind2  12288  prmpwdvds  12524  lgsdir2lem4  15272