Theorem vtoclga 3576

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815

This theorem is referenced by:  vtocl2ga  3577  vtocl3ga  3582  vtoclri  3589  disjxiun  5139  wfis3  6381  opabiota  6990  fvmpt3  7019  fvmptss  7027  fnressn  7177  fressnfv  7179  caovord  7645  caovmo  7671  ordunisuc  7853  tfis3  7880  fpr2a  8328  frrdmcl  8334  wfr2aOLD  8367  onfununi  8382  smogt  8408  tz7.44-1  8447  tz7.44-2  8448  tz7.44-3  8449  nnacl  8650  nnmcl  8651  nnecl  8652  nnacom  8656  nnaass  8661  nndi  8662  nnmass  8663  nnmsucr  8664  nnmcom  8665  nnmordi  8670  ixpfn  8944  findcard  9204  findcard2  9205  marypha1  9475  cantnfle  9712  cantnflem1  9730  cnfcom  9741  frr2  9801  fseqenlem1  10065  nnadju  10239  ackbij1lem8  10267  cardcf  10293  cfsmolem  10311  wunex2  10779  ingru  10856  recrecnq  11008  prlem934  11074  nn1suc  12289  uzind4s2  12952  rpnnen1lem6  13025  cnref1o  13028  xmulasslem  13328  om2uzsuci  13990  expcl2lem  14115  hashpw  14476  seqcoll  14504  climub  15699  climserle  15700  sumrblem  15748  fsumcvg  15749  summolem2a  15752  infcvgaux2i  15895  prodfn0  15931  prodfrec  15932  prodrblem  15966  fprodcvg  15967  prodmolem2a  15971  divalglem8  16438  bezoutlem1  16577  alginv  16613  algcvg  16614  algcvga  16617  algfx  16618  prmind2  16723  prmpwdvds  16943  cnextfvval  24074  xrsxmet  24832  xrhmeo  24978  cmetcaulem  25323  bcth3  25366  itg2addlem  25794  taylfval  26401  sinord  26577  logexprlim  27270  lgsdir2lem4  27373  noseqind  28299  hlim2  31212  elnlfn  31948  lnconi  32053  chirredlem3  32412  chirredlem4  32413  cnre2csqlem  33910  eulerpartlemsf  34362  eulerpartlemn  34384  bnj1321  35042  bnj1418  35055  subfacp1lem1  35185  nn0prpwlem  36324  findreccl  36455  weiunlem2  36465  mptsnunlem  37340  rdgeqoa  37372  domalom  37406  poimirlem22  37650  poimirlem26  37654  mblfinlem3  37667  mblfinlem4  37668  ismblfin  37669  ftc1anclem3  37703  ftc1anclem8  37708  sdclem2  37750  iscringd  38006  renegclALT  38965  zindbi  42963  fmuldfeq  45603  sumnnodd  45650  iblspltprt  45993  stoweidlem2  46022  stoweidlem17  46037  stoweidlem21  46041  stoweidlem43  46063  stoweidlem51  46071  wallispi  46090  upwordisword  46901