Theorem vtoclga 3540

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2180 and ax-11 2197. (Revised by GG, 20-Aug-2023.)

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		eleq1 2852	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3521	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 53	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  vtocl2ga  3541  vtocl3ga  3544  vtoclri  3548  disjxiun  5103  wfis3  6375  opabiota  6987  fvmpt3  7018  fvmptss  7026  fnressn  7183  fressnfv  7185  caovord  7653  caovmo  7679  tfis3  7890  fpr2a  8345  frrdmcl  8351  onfununi  8374  smogt  8400  tz7.44-1  8439  tz7.44-2  8440  tz7.44-3  8441  nnacl  8645  nnmcl  8646  nnecl  8647  nnacom  8651  nnaass  8656  nndi  8657  nnmass  8658  nnmsucr  8659  nnmcom  8660  nnmordi  8665  ixpfn  8956  findcard  9204  findcard2  9205  marypha1  9450  cantnfle  9696  cantnflem1  9714  cnfcom  9725  frr2  9788  fseqenlem1  10127  nnadju  10300  ackbij1lem8  10328  cardcf  10353  cfsmolem  10372  wunex2  10847  ingru  10924  recrecnq  11076  prlem934  11142  nn1suc  12381  uzind4s2  13060  rpnnen1lem6  13134  cnref1o  13137  xmulasslem  13439  om2uzsuci  14115  expcl2lem  14240  hashpw  14605  seqcoll  14633  climub  15855  climserle  15856  sumrblem  15903  fsumcvg  15904  summolem2a  15907  infcvgaux2i  16053  prodfn0  16089  prodfrec  16090  prodrblem  16122  fprodcvg  16123  prodmolem2a  16127  divalglem8  16596  bezoutlem1  16738  alginv  16776  algcvg  16777  algcvga  16780  algfx  16781  prmind2  16886  prmpwdvds  17108  cnextfvval  24411  xrsxmet  25156  xrhmeo  25294  cmetcaulem  25636  bcth3  25679  itg2addlem  26106  taylfval  26713  sinord  26889  logexprlim  27579  lgsdir2lem4  27682  noseqind  28705  hlim2  31821  elnlfn  32557  lnconi  32662  chirredlem3  33021  chirredlem4  33022  cnre2csqlem  34609  eulerpartlemsf  35058  eulerpartlemn  35080  bnj1321  35724  bnj1418  35737  subfacp1lem1  36110  nn0prpwlem  37287  findreccl  37418  weiunlem  37428  mptsnunlem  38452  rdgeqoa  38484  domalom  38518  poimirlem22  38751  poimirlem26  38755  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  ftc1anclem3  38804  ftc1anclem8  38809  sdclem2  38867  iscringd  39123  renegclALT  40211  zindbi  44144  fmuldfeq  46798  sumnnodd  46845  iblspltprt  47186  stoweidlem2  47215  stoweidlem17  47230  stoweidlem21  47234  stoweidlem43  47256  stoweidlem51  47264  wallispi  47283