Theorem vtoclga 3520

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 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3499	. 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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  vtocl2ga  3521  vtocl3ga  3526  vtoclri  3532  disjxiun  5082  wfis3  6321  opabiota  6922  fvmpt3  6952  fvmptss  6960  fnressn  7112  fressnfv  7114  caovord  7578  caovmo  7604  ordunisuc  7783  tfis3  7809  fpr2a  8252  frrdmcl  8258  onfununi  8281  smogt  8307  tz7.44-1  8345  tz7.44-2  8346  tz7.44-3  8347  nnacl  8547  nnmcl  8548  nnecl  8549  nnacom  8553  nnaass  8558  nndi  8559  nnmass  8560  nnmsucr  8561  nnmcom  8562  nnmordi  8567  ixpfn  8851  findcard  9098  findcard2  9099  marypha1  9347  cantnfle  9592  cantnflem1  9610  cnfcom  9621  frr2  9684  fseqenlem1  9946  nnadju  10120  ackbij1lem8  10148  cardcf  10174  cfsmolem  10192  wunex2  10661  ingru  10738  recrecnq  10890  prlem934  10956  nn1suc  12196  uzind4s2  12859  rpnnen1lem6  12932  cnref1o  12935  xmulasslem  13237  om2uzsuci  13910  expcl2lem  14035  hashpw  14398  seqcoll  14426  climub  15624  climserle  15625  sumrblem  15673  fsumcvg  15674  summolem2a  15677  infcvgaux2i  15823  prodfn0  15859  prodfrec  15860  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  divalglem8  16369  bezoutlem1  16508  alginv  16544  algcvg  16545  algcvga  16548  algfx  16549  prmind2  16654  prmpwdvds  16875  cnextfvval  24030  xrsxmet  24775  xrhmeo  24913  cmetcaulem  25255  bcth3  25298  itg2addlem  25725  taylfval  26324  sinord  26498  logexprlim  27188  lgsdir2lem4  27291  noseqind  28284  hlim2  31263  elnlfn  31999  lnconi  32104  chirredlem3  32463  chirredlem4  32464  cnre2csqlem  34054  eulerpartlemsf  34503  eulerpartlemn  34525  bnj1321  35169  bnj1418  35182  subfacp1lem1  35361  nn0prpwlem  36504  findreccl  36635  weiunlem  36645  mptsnunlem  37654  rdgeqoa  37686  domalom  37720  poimirlem22  37963  poimirlem26  37967  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  ftc1anclem3  38016  ftc1anclem8  38021  sdclem2  38063  iscringd  38319  renegclALT  39409  zindbi  43374  fmuldfeq  46013  sumnnodd  46060  iblspltprt  46401  stoweidlem2  46430  stoweidlem17  46445  stoweidlem21  46449  stoweidlem43  46471  stoweidlem51  46479  wallispi  46498