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  9600  cantnflem1  9618  cnfcom  9629  frr2  9689  fseqenlem1  9953  nnadju  10127  ackbij1lem8  10155  cardcf  10181  cfsmolem  10199  wunex2  10667  ingru  10744  recrecnq  10896  prlem934  10962  nn1suc  12184  uzind4s2  12844  rpnnen1lem6  12917  cnref1o  12920  xmulasslem  13221  om2uzsuci  13889  expcl2lem  14014  hashpw  14377  seqcoll  14405  climub  15604  climserle  15605  sumrblem  15653  fsumcvg  15654  summolem2a  15657  infcvgaux2i  15800  prodfn0  15836  prodfrec  15837  prodrblem  15871  fprodcvg  15872  prodmolem2a  15876  divalglem8  16346  bezoutlem1  16485  alginv  16521  algcvg  16522  algcvga  16525  algfx  16526  prmind2  16631  prmpwdvds  16851  cnextfvval  23985  xrsxmet  24731  xrhmeo  24877  cmetcaulem  25221  bcth3  25264  itg2addlem  25692  taylfval  26299  sinord  26476  logexprlim  27169  lgsdir2lem4  27272  noseqind  28226  hlim2  31171  elnlfn  31907  lnconi  32012  chirredlem3  32371  chirredlem4  32372  cnre2csqlem  33893  eulerpartlemsf  34343  eulerpartlemn  34365  bnj1321  35010  bnj1418  35023  subfacp1lem1  35159  nn0prpwlem  36303  findreccl  36434  weiunlem2  36444  mptsnunlem  37319  rdgeqoa  37351  domalom  37385  poimirlem22  37629  poimirlem26  37633  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  ftc1anclem3  37682  ftc1anclem8  37687  sdclem2  37729  iscringd  37985  renegclALT  38949  zindbi  42928  fmuldfeq  45574  sumnnodd  45621  iblspltprt  45964  stoweidlem2  45993  stoweidlem17  46008  stoweidlem21  46012  stoweidlem43  46034  stoweidlem51  46042  wallispi  46061  upwordisword  46872