Theorem vtoclga 3534

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2147 and ax-11 2163. (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 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3513	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 52	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  vtocl2ga  3535  vtocl3ga  3540  vtoclri  3546  disjxiun  5097  wfis3  6325  opabiota  6926  fvmpt3  6956  fvmptss  6964  fnressn  7115  fressnfv  7117  caovord  7581  caovmo  7607  ordunisuc  7786  tfis3  7812  fpr2a  8256  frrdmcl  8262  onfununi  8285  smogt  8311  tz7.44-1  8349  tz7.44-2  8350  tz7.44-3  8351  nnacl  8551  nnmcl  8552  nnecl  8553  nnacom  8557  nnaass  8562  nndi  8563  nnmass  8564  nnmsucr  8565  nnmcom  8566  nnmordi  8571  ixpfn  8855  findcard  9102  findcard2  9103  marypha1  9351  cantnfle  9594  cantnflem1  9612  cnfcom  9623  frr2  9686  fseqenlem1  9948  nnadju  10122  ackbij1lem8  10150  cardcf  10176  cfsmolem  10194  wunex2  10663  ingru  10740  recrecnq  10892  prlem934  10958  nn1suc  12181  uzind4s2  12836  rpnnen1lem6  12909  cnref1o  12912  xmulasslem  13214  om2uzsuci  13885  expcl2lem  14010  hashpw  14373  seqcoll  14401  climub  15599  climserle  15600  sumrblem  15648  fsumcvg  15649  summolem2a  15652  infcvgaux2i  15795  prodfn0  15831  prodfrec  15832  prodrblem  15866  fprodcvg  15867  prodmolem2a  15871  divalglem8  16341  bezoutlem1  16480  alginv  16516  algcvg  16517  algcvga  16520  algfx  16521  prmind2  16626  prmpwdvds  16846  cnextfvval  24026  xrsxmet  24771  xrhmeo  24917  cmetcaulem  25261  bcth3  25304  itg2addlem  25732  taylfval  26339  sinord  26516  logexprlim  27209  lgsdir2lem4  27312  noseqind  28305  hlim2  31286  elnlfn  32022  lnconi  32127  chirredlem3  32486  chirredlem4  32487  cnre2csqlem  34094  eulerpartlemsf  34543  eulerpartlemn  34565  bnj1321  35209  bnj1418  35222  subfacp1lem1  35401  nn0prpwlem  36544  findreccl  36675  weiunlem  36685  mptsnunlem  37620  rdgeqoa  37652  domalom  37686  poimirlem22  37922  poimirlem26  37926  mblfinlem3  37939  mblfinlem4  37940  ismblfin  37941  ftc1anclem3  37975  ftc1anclem8  37980  sdclem2  38022  iscringd  38278  renegclALT  39368  zindbi  43332  fmuldfeq  45972  sumnnodd  46019  iblspltprt  46360  stoweidlem2  46389  stoweidlem17  46404  stoweidlem21  46408  stoweidlem43  46430  stoweidlem51  46438  wallispi  46457