Theorem vtoclga 3574

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  vtocl2ga  3575  vtoclri  3585  disjxiun  5063  wfis3  6189  opabiota  6746  fvmpt3  6772  fvmptss  6780  fnressn  6920  fressnfv  6922  caovord  7359  caovmo  7385  ordunisuc  7547  tfis3  7572  wfr2a  7972  onfununi  7978  smogt  8004  tz7.44-1  8042  tz7.44-2  8043  tz7.44-3  8044  nnacl  8237  nnmcl  8238  nnecl  8239  nnacom  8243  nnaass  8248  nndi  8249  nnmass  8250  nnmsucr  8251  nnmcom  8252  nnmordi  8257  ixpfn  8467  findcard  8757  findcard2  8758  marypha1  8898  cantnfle  9134  cantnflem1  9152  cnfcom  9163  fseqenlem1  9450  ackbij1lem8  9649  cardcf  9674  cfsmolem  9692  wunex2  10160  ingru  10237  recrecnq  10389  prlem934  10455  nn1suc  11660  uzind4s2  12310  rpnnen1lem6  12382  cnref1o  12385  xmulasslem  12679  om2uzsuci  13317  expcl2lem  13442  hashpw  13798  seqcoll  13823  climub  15018  climserle  15019  sumrblem  15068  fsumcvg  15069  summolem2a  15072  infcvgaux2i  15213  prodfn0  15250  prodfrec  15251  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  divalglem8  15751  bezoutlem1  15887  alginv  15919  algcvg  15920  algcvga  15923  algfx  15924  prmind2  16029  prmpwdvds  16240  cnextfvval  22673  xrsxmet  23417  xrhmeo  23550  cmetcaulem  23891  bcth3  23934  itg2addlem  24359  taylfval  24947  sinord  25118  logexprlim  25801  lgsdir2lem4  25904  hlim2  28969  elnlfn  29705  lnconi  29810  chirredlem3  30169  chirredlem4  30170  cnre2csqlem  31153  eulerpartlemsf  31617  eulerpartlemn  31639  bnj1321  32299  bnj1418  32312  subfacp1lem1  32426  frins3  33093  fpr2  33140  frr2  33145  nn0prpwlem  33670  findreccl  33801  mptsnunlem  34622  rdgeqoa  34654  domalom  34688  poimirlem22  34929  poimirlem26  34933  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  ftc1anclem3  34984  ftc1anclem8  34989  sdclem2  35032  iscringd  35291  renegclALT  36114  zindbi  39563  fmuldfeq  41884  sumnnodd  41931  iblspltprt  42278  stoweidlem2  42307  stoweidlem17  42322  stoweidlem21  42326  stoweidlem43  42348  stoweidlem51  42356  wallispi  42375