Theorem vtoclga 3543

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  vtocl2ga  3544  vtocl3ga  3549  vtoclri  3556  disjxiun  5104  wfis3  6330  opabiota  6943  fvmpt3  6972  fvmptss  6980  fnressn  7130  fressnfv  7132  caovord  7600  caovmo  7626  ordunisuc  7807  tfis3  7834  fpr2a  8281  frrdmcl  8287  onfununi  8310  smogt  8336  tz7.44-1  8374  tz7.44-2  8375  tz7.44-3  8376  nnacl  8575  nnmcl  8576  nnecl  8577  nnacom  8581  nnaass  8586  nndi  8587  nnmass  8588  nnmsucr  8589  nnmcom  8590  nnmordi  8595  ixpfn  8876  findcard  9127  findcard2  9128  marypha1  9385  cantnfle  9624  cantnflem1  9642  cnfcom  9653  frr2  9713  fseqenlem1  9977  nnadju  10151  ackbij1lem8  10179  cardcf  10205  cfsmolem  10223  wunex2  10691  ingru  10768  recrecnq  10920  prlem934  10986  nn1suc  12208  uzind4s2  12868  rpnnen1lem6  12941  cnref1o  12944  xmulasslem  13245  om2uzsuci  13913  expcl2lem  14038  hashpw  14401  seqcoll  14429  climub  15628  climserle  15629  sumrblem  15677  fsumcvg  15678  summolem2a  15681  infcvgaux2i  15824  prodfn0  15860  prodfrec  15861  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  divalglem8  16370  bezoutlem1  16509  alginv  16545  algcvg  16546  algcvga  16549  algfx  16550  prmind2  16655  prmpwdvds  16875  cnextfvval  23952  xrsxmet  24698  xrhmeo  24844  cmetcaulem  25188  bcth3  25231  itg2addlem  25659  taylfval  26266  sinord  26443  logexprlim  27136  lgsdir2lem4  27239  noseqind  28186  hlim2  31121  elnlfn  31857  lnconi  31962  chirredlem3  32321  chirredlem4  32322  cnre2csqlem  33900  eulerpartlemsf  34350  eulerpartlemn  34372  bnj1321  35017  bnj1418  35030  subfacp1lem1  35166  nn0prpwlem  36310  findreccl  36441  weiunlem2  36451  mptsnunlem  37326  rdgeqoa  37358  domalom  37392  poimirlem22  37636  poimirlem26  37640  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  ftc1anclem3  37689  ftc1anclem8  37694  sdclem2  37736  iscringd  37992  renegclALT  38956  zindbi  42935  fmuldfeq  45581  sumnnodd  45628  iblspltprt  45971  stoweidlem2  46000  stoweidlem17  46015  stoweidlem21  46019  stoweidlem43  46041  stoweidlem51  46049  wallispi  46068  upwordisword  46879