Theorem vtoclga 3565

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810

This theorem is referenced by:  vtocl2ga  3566  vtoclri  3576  disjxiun  5145  wfis3  6362  opabiota  6974  fvmpt3  7002  fvmptss  7010  fnressn  7158  fressnfv  7160  caovord  7620  caovmo  7646  ordunisuc  7822  tfis3  7849  fpr2a  8289  frrdmcl  8295  wfr2aOLD  8328  onfununi  8343  smogt  8369  tz7.44-1  8408  tz7.44-2  8409  tz7.44-3  8410  nnacl  8613  nnmcl  8614  nnecl  8615  nnacom  8619  nnaass  8624  nndi  8625  nnmass  8626  nnmsucr  8627  nnmcom  8628  nnmordi  8633  ixpfn  8899  findcard  9165  findcard2  9166  findcard2OLD  9286  marypha1  9431  cantnfle  9668  cantnflem1  9686  cnfcom  9697  frr2  9757  fseqenlem1  10021  nnadju  10194  ackbij1lem8  10224  cardcf  10249  cfsmolem  10267  wunex2  10735  ingru  10812  recrecnq  10964  prlem934  11030  nn1suc  12236  uzind4s2  12895  rpnnen1lem6  12968  cnref1o  12971  xmulasslem  13266  om2uzsuci  13915  expcl2lem  14041  hashpw  14398  seqcoll  14427  climub  15610  climserle  15611  sumrblem  15659  fsumcvg  15660  summolem2a  15663  infcvgaux2i  15806  prodfn0  15842  prodfrec  15843  prodrblem  15875  fprodcvg  15876  prodmolem2a  15880  divalglem8  16345  bezoutlem1  16483  alginv  16514  algcvg  16515  algcvga  16518  algfx  16519  prmind2  16624  prmpwdvds  16839  cnextfvval  23576  xrsxmet  24332  xrhmeo  24469  cmetcaulem  24812  bcth3  24855  itg2addlem  25283  taylfval  25878  sinord  26050  logexprlim  26735  lgsdir2lem4  26838  hlim2  30483  elnlfn  31219  lnconi  31324  chirredlem3  31683  chirredlem4  31684  cnre2csqlem  32959  eulerpartlemsf  33427  eulerpartlemn  33449  bnj1321  34107  bnj1418  34120  subfacp1lem1  34239  nn0prpwlem  35293  findreccl  35424  mptsnunlem  36305  rdgeqoa  36337  domalom  36371  poimirlem22  36596  poimirlem26  36600  mblfinlem3  36613  mblfinlem4  36614  ismblfin  36615  ftc1anclem3  36649  ftc1anclem8  36654  sdclem2  36696  iscringd  36952  renegclALT  37919  zindbi  41767  fmuldfeq  44378  sumnnodd  44425  iblspltprt  44768  stoweidlem2  44797  stoweidlem17  44812  stoweidlem21  44816  stoweidlem43  44838  stoweidlem51  44846  wallispi  44865  upwordisword  45674