Theorem vtoclga 3561

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810

This theorem is referenced by:  vtocl2ga  3562  vtocl3ga  3567  vtoclri  3574  disjxiun  5121  wfis3  6355  opabiota  6966  fvmpt3  6995  fvmptss  7003  fnressn  7153  fressnfv  7155  caovord  7623  caovmo  7649  ordunisuc  7831  tfis3  7858  fpr2a  8306  frrdmcl  8312  wfr2aOLD  8345  onfununi  8360  smogt  8386  tz7.44-1  8425  tz7.44-2  8426  tz7.44-3  8427  nnacl  8628  nnmcl  8629  nnecl  8630  nnacom  8634  nnaass  8639  nndi  8640  nnmass  8641  nnmsucr  8642  nnmcom  8643  nnmordi  8648  ixpfn  8922  findcard  9182  findcard2  9183  marypha1  9451  cantnfle  9690  cantnflem1  9708  cnfcom  9719  frr2  9779  fseqenlem1  10043  nnadju  10217  ackbij1lem8  10245  cardcf  10271  cfsmolem  10289  wunex2  10757  ingru  10834  recrecnq  10986  prlem934  11052  nn1suc  12267  uzind4s2  12930  rpnnen1lem6  13003  cnref1o  13006  xmulasslem  13306  om2uzsuci  13971  expcl2lem  14096  hashpw  14459  seqcoll  14487  climub  15683  climserle  15684  sumrblem  15732  fsumcvg  15733  summolem2a  15736  infcvgaux2i  15879  prodfn0  15915  prodfrec  15916  prodrblem  15950  fprodcvg  15951  prodmolem2a  15955  divalglem8  16424  bezoutlem1  16563  alginv  16599  algcvg  16600  algcvga  16603  algfx  16604  prmind2  16709  prmpwdvds  16929  cnextfvval  24008  xrsxmet  24754  xrhmeo  24900  cmetcaulem  25245  bcth3  25288  itg2addlem  25716  taylfval  26323  sinord  26500  logexprlim  27193  lgsdir2lem4  27296  noseqind  28243  hlim2  31178  elnlfn  31914  lnconi  32019  chirredlem3  32378  chirredlem4  32379  cnre2csqlem  33946  eulerpartlemsf  34396  eulerpartlemn  34418  bnj1321  35063  bnj1418  35076  subfacp1lem1  35206  nn0prpwlem  36345  findreccl  36476  weiunlem2  36486  mptsnunlem  37361  rdgeqoa  37393  domalom  37427  poimirlem22  37671  poimirlem26  37675  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  ftc1anclem3  37724  ftc1anclem8  37729  sdclem2  37771  iscringd  38027  renegclALT  38986  zindbi  42945  fmuldfeq  45592  sumnnodd  45639  iblspltprt  45982  stoweidlem2  46011  stoweidlem17  46026  stoweidlem21  46030  stoweidlem43  46052  stoweidlem51  46060  wallispi  46079  upwordisword  46890