Theorem vtoclga 3540

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 3517	. 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  3541  vtocl3ga  3546  vtoclri  3553  disjxiun  5099  wfis3  6318  opabiota  6925  fvmpt3  6954  fvmptss  6962  fnressn  7112  fressnfv  7114  caovord  7580  caovmo  7606  ordunisuc  7787  tfis3  7814  fpr2a  8258  frrdmcl  8264  onfununi  8287  smogt  8313  tz7.44-1  8351  tz7.44-2  8352  tz7.44-3  8353  nnacl  8552  nnmcl  8553  nnecl  8554  nnacom  8558  nnaass  8563  nndi  8564  nnmass  8565  nnmsucr  8566  nnmcom  8567  nnmordi  8572  ixpfn  8853  findcard  9104  findcard2  9105  marypha1  9361  cantnfle  9602  cantnflem1  9620  cnfcom  9631  frr2  9691  fseqenlem1  9955  nnadju  10129  ackbij1lem8  10157  cardcf  10183  cfsmolem  10201  wunex2  10669  ingru  10746  recrecnq  10898  prlem934  10964  nn1suc  12186  uzind4s2  12846  rpnnen1lem6  12919  cnref1o  12922  xmulasslem  13223  om2uzsuci  13891  expcl2lem  14016  hashpw  14379  seqcoll  14407  climub  15605  climserle  15606  sumrblem  15654  fsumcvg  15655  summolem2a  15658  infcvgaux2i  15801  prodfn0  15837  prodfrec  15838  prodrblem  15872  fprodcvg  15873  prodmolem2a  15877  divalglem8  16347  bezoutlem1  16486  alginv  16522  algcvg  16523  algcvga  16526  algfx  16527  prmind2  16632  prmpwdvds  16852  cnextfvval  23986  xrsxmet  24732  xrhmeo  24878  cmetcaulem  25222  bcth3  25265  itg2addlem  25693  taylfval  26300  sinord  26477  logexprlim  27170  lgsdir2lem4  27273  noseqind  28227  hlim2  31172  elnlfn  31908  lnconi  32013  chirredlem3  32372  chirredlem4  32373  cnre2csqlem  33894  eulerpartlemsf  34344  eulerpartlemn  34366  bnj1321  35011  bnj1418  35024  subfacp1lem1  35160  nn0prpwlem  36304  findreccl  36435  weiunlem2  36445  mptsnunlem  37320  rdgeqoa  37352  domalom  37386  poimirlem22  37630  poimirlem26  37634  mblfinlem3  37647  mblfinlem4  37648  ismblfin  37649  ftc1anclem3  37683  ftc1anclem8  37688  sdclem2  37730  iscringd  37986  renegclALT  38950  zindbi  42929  fmuldfeq  45575  sumnnodd  45622  iblspltprt  45965  stoweidlem2  45994  stoweidlem17  46009  stoweidlem21  46013  stoweidlem43  46035  stoweidlem51  46043  wallispi  46062  upwordisword  46873