Theorem vtoclga 3489

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  vtocl2ga  3490  vtoclri  3501  disjxiun  5050  wfis3  6211  opabiota  6794  fvmpt3  6822  fvmptss  6830  fnressn  6973  fressnfv  6975  caovord  7419  caovmo  7445  ordunisuc  7611  tfis3  7636  fpr2  8044  wfr2a  8072  onfununi  8078  smogt  8104  tz7.44-1  8142  tz7.44-2  8143  tz7.44-3  8144  nnacl  8339  nnmcl  8340  nnecl  8341  nnacom  8345  nnaass  8350  nndi  8351  nnmass  8352  nnmsucr  8353  nnmcom  8354  nnmordi  8359  ixpfn  8584  findcard  8841  findcard2  8842  findcard2OLD  8913  marypha1  9050  cantnfle  9286  cantnflem1  9304  cnfcom  9315  frr2  9376  fseqenlem1  9638  nnadju  9811  ackbij1lem8  9841  cardcf  9866  cfsmolem  9884  wunex2  10352  ingru  10429  recrecnq  10581  prlem934  10647  nn1suc  11852  uzind4s2  12505  rpnnen1lem6  12578  cnref1o  12581  xmulasslem  12875  om2uzsuci  13521  expcl2lem  13647  hashpw  14003  seqcoll  14030  climub  15225  climserle  15226  sumrblem  15275  fsumcvg  15276  summolem2a  15279  infcvgaux2i  15422  prodfn0  15458  prodfrec  15459  prodrblem  15491  fprodcvg  15492  prodmolem2a  15496  divalglem8  15961  bezoutlem1  16099  alginv  16132  algcvg  16133  algcvga  16136  algfx  16137  prmind2  16242  prmpwdvds  16457  cnextfvval  22962  xrsxmet  23706  xrhmeo  23843  cmetcaulem  24185  bcth3  24228  itg2addlem  24656  taylfval  25251  sinord  25423  logexprlim  26106  lgsdir2lem4  26209  hlim2  29273  elnlfn  30009  lnconi  30114  chirredlem3  30473  chirredlem4  30474  cnre2csqlem  31574  eulerpartlemsf  32038  eulerpartlemn  32060  bnj1321  32720  bnj1418  32733  subfacp1lem1  32854  nn0prpwlem  34248  findreccl  34379  mptsnunlem  35246  rdgeqoa  35278  domalom  35312  poimirlem22  35536  poimirlem26  35540  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  ftc1anclem3  35589  ftc1anclem8  35594  sdclem2  35637  iscringd  35893  renegclALT  36714  zindbi  40471  fmuldfeq  42799  sumnnodd  42846  iblspltprt  43189  stoweidlem2  43218  stoweidlem17  43233  stoweidlem21  43237  stoweidlem43  43259  stoweidlem51  43267  wallispi  43286