Theorem vtoclga 2699

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1296   ∈ wcel 1445

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635

This theorem is referenced by:  vtoclri  2708  ssuni  3697  ordtriexmid  4366  onsucsssucexmid  4371  tfis3  4429  fvmpt3  5418  fvmptssdm  5423  fnressn  5522  fressnfv  5523  caovord  5854  caovimo  5876  tfrlem1  6111  nnacl  6281  nnmcl  6282  nnacom  6285  nnaass  6286  nndi  6287  nnmass  6288  nnmsucr  6289  nnmcom  6290  nnsucsssuc  6293  nntri3or  6294  nnaordi  6307  nnaword  6310  nnmordi  6315  nnaordex  6326  ixpfn  6501  findcard  6684  findcard2  6685  findcard2s  6686  exmidomni  6885  indpi  6998  prarloclem3  7153  uzind4s2  9178  cnref1o  9232  frec2uzrdg  9965  expcl2lemap  10098  seq3coll  10378  climub  10903  climserle  10904  fsum3cvg  10936  summodclem2a  10940  alginv  11472  algcvg  11473  algcvga  11476  algfx  11477  prmind2  11545