Theorem vtoclga 3589

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  vtocl2ga  3590  vtocl3ga  3595  vtoclri  3603  disjxiun  5163  wfis3  6393  opabiota  7004  fvmpt3  7033  fvmptss  7041  fnressn  7192  fressnfv  7194  caovord  7661  caovmo  7687  ordunisuc  7868  tfis3  7895  fpr2a  8343  frrdmcl  8349  wfr2aOLD  8382  onfununi  8397  smogt  8423  tz7.44-1  8462  tz7.44-2  8463  tz7.44-3  8464  nnacl  8667  nnmcl  8668  nnecl  8669  nnacom  8673  nnaass  8678  nndi  8679  nnmass  8680  nnmsucr  8681  nnmcom  8682  nnmordi  8687  ixpfn  8961  findcard  9229  findcard2  9230  marypha1  9503  cantnfle  9740  cantnflem1  9758  cnfcom  9769  frr2  9829  fseqenlem1  10093  nnadju  10267  ackbij1lem8  10295  cardcf  10321  cfsmolem  10339  wunex2  10807  ingru  10884  recrecnq  11036  prlem934  11102  nn1suc  12315  uzind4s2  12974  rpnnen1lem6  13047  cnref1o  13050  xmulasslem  13347  om2uzsuci  13999  expcl2lem  14124  hashpw  14485  seqcoll  14513  climub  15710  climserle  15711  sumrblem  15759  fsumcvg  15760  summolem2a  15763  infcvgaux2i  15906  prodfn0  15942  prodfrec  15943  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  divalglem8  16448  bezoutlem1  16586  alginv  16622  algcvg  16623  algcvga  16626  algfx  16627  prmind2  16732  prmpwdvds  16951  cnextfvval  24094  xrsxmet  24850  xrhmeo  24996  cmetcaulem  25341  bcth3  25384  itg2addlem  25813  taylfval  26418  sinord  26594  logexprlim  27287  lgsdir2lem4  27390  noseqind  28316  hlim2  31224  elnlfn  31960  lnconi  32065  chirredlem3  32424  chirredlem4  32425  cnre2csqlem  33856  eulerpartlemsf  34324  eulerpartlemn  34346  bnj1321  35003  bnj1418  35016  subfacp1lem1  35147  nn0prpwlem  36288  findreccl  36419  weiunlem2  36429  mptsnunlem  37304  rdgeqoa  37336  domalom  37370  poimirlem22  37602  poimirlem26  37606  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  ftc1anclem3  37655  ftc1anclem8  37660  sdclem2  37702  iscringd  37958  renegclALT  38919  zindbi  42903  fmuldfeq  45504  sumnnodd  45551  iblspltprt  45894  stoweidlem2  45923  stoweidlem17  45938  stoweidlem21  45942  stoweidlem43  45964  stoweidlem51  45972  wallispi  45991  upwordisword  46800