Theorem vtoclga 3410

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630   ∈ wcel 2137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340

This theorem is referenced by:  vtoclri  3421  ssuniOLD  4610  disjxiun  4799  wfis3  5880  opabiota  6421  fvmpt3  6446  fvmptss  6452  fnressn  6586  fressnfv  6588  caovord  7008  caovmo  7034  ordunisuc  7195  tfis3  7220  wfr2a  7599  onfununi  7605  smogt  7631  tz7.44-1  7669  tz7.44-2  7670  tz7.44-3  7671  nnacl  7858  nnmcl  7859  nnecl  7860  nnacom  7864  nnaass  7869  nndi  7870  nnmass  7871  nnmsucr  7872  nnmcom  7873  nnmordi  7878  ixpfn  8078  findcard  8362  findcard2  8363  marypha1  8503  cantnfle  8739  cantnflem1  8757  cnfcom  8768  fseqenlem1  9035  ackbij1lem5  9236  ackbij1lem8  9239  cardcf  9264  cfsmolem  9282  wunex2  9750  ingru  9827  recrecnq  9979  prlem934  10045  nn1suc  11231  uzind4s2  11940  rpnnen1lem6  12010  rpnnen1OLD  12016  cnref1o  12018  xmulasslem  12306  om2uzsuci  12939  expcl2lem  13064  hashmap  13412  hashpw  13413  seqcoll  13438  climub  14589  climserle  14590  sumrblem  14639  fsumcvg  14640  summolem2a  14643  infcvgaux2i  14787  prodfn0  14823  prodfrec  14824  prodrblem  14856  fprodcvg  14857  prodmolem2a  14861  divalglem8  15323  bezoutlem1  15456  alginv  15488  algcvg  15489  algcvga  15492  algfx  15493  prmind2  15598  prmpwdvds  15808  cnextfvval  22068  xrsxmet  22811  xrhmeo  22944  cmetcaulem  23284  bcth3  23326  itg2addlem  23722  taylfval  24310  sinord  24477  logexprlim  25147  lgsdir2lem4  25250  hlim2  28356  elnlfn  29094  lnconi  29199  chirredlem3  29558  chirredlem4  29559  cnre2csqlem  30263  eulerpartlemsf  30728  eulerpartlemn  30750  bnj1321  31400  bnj1418  31413  subfacp1lem1  31466  frins3  32055  nn0prpwlem  32621  findreccl  32756  mptsnunlem  33494  rdgeqoa  33527  poimirlem22  33742  poimirlem26  33746  mblfinlem3  33759  mblfinlem4  33760  ismblfin  33761  ftc1anclem3  33798  ftc1anclem8  33803  sdclem2  33849  iscringd  34108  renegclALT  34750  zindbi  38011  fmuldfeq  40316  sumnnodd  40363  iblspltprt  40690  stoweidlem2  40720  stoweidlem17  40735  stoweidlem21  40739  stoweidlem43  40761  stoweidlem51  40769  wallispi  40788