Theorem vtoclga 3533

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  vtocl2ga  3534  vtocl3ga  3539  vtoclri  3545  disjxiun  5096  wfis3  6316  opabiota  6917  fvmpt3  6947  fvmptss  6955  fnressn  7105  fressnfv  7107  caovord  7571  caovmo  7597  ordunisuc  7776  tfis3  7802  fpr2a  8246  frrdmcl  8252  onfununi  8275  smogt  8301  tz7.44-1  8339  tz7.44-2  8340  tz7.44-3  8341  nnacl  8541  nnmcl  8542  nnecl  8543  nnacom  8547  nnaass  8552  nndi  8553  nnmass  8554  nnmsucr  8555  nnmcom  8556  nnmordi  8561  ixpfn  8845  findcard  9092  findcard2  9093  marypha1  9341  cantnfle  9584  cantnflem1  9602  cnfcom  9613  frr2  9676  fseqenlem1  9938  nnadju  10112  ackbij1lem8  10140  cardcf  10166  cfsmolem  10184  wunex2  10653  ingru  10730  recrecnq  10882  prlem934  10948  nn1suc  12171  uzind4s2  12826  rpnnen1lem6  12899  cnref1o  12902  xmulasslem  13204  om2uzsuci  13875  expcl2lem  14000  hashpw  14363  seqcoll  14391  climub  15589  climserle  15590  sumrblem  15638  fsumcvg  15639  summolem2a  15642  infcvgaux2i  15785  prodfn0  15821  prodfrec  15822  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  divalglem8  16331  bezoutlem1  16470  alginv  16506  algcvg  16507  algcvga  16510  algfx  16511  prmind2  16616  prmpwdvds  16836  cnextfvval  24013  xrsxmet  24758  xrhmeo  24904  cmetcaulem  25248  bcth3  25291  itg2addlem  25719  taylfval  26326  sinord  26503  logexprlim  27196  lgsdir2lem4  27299  noseqind  28273  hlim2  31250  elnlfn  31986  lnconi  32091  chirredlem3  32450  chirredlem4  32451  cnre2csqlem  34048  eulerpartlemsf  34497  eulerpartlemn  34519  bnj1321  35164  bnj1418  35177  subfacp1lem1  35354  nn0prpwlem  36497  findreccl  36628  weiunlem2  36638  mptsnunlem  37514  rdgeqoa  37546  domalom  37580  poimirlem22  37814  poimirlem26  37818  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  ftc1anclem3  37867  ftc1anclem8  37872  sdclem2  37914  iscringd  38170  renegclALT  39260  zindbi  43224  fmuldfeq  45865  sumnnodd  45912  iblspltprt  46253  stoweidlem2  46282  stoweidlem17  46297  stoweidlem21  46301  stoweidlem43  46323  stoweidlem51  46331  wallispi  46350