Theorem vtoclga 3548

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844

This theorem is referenced by:  vtocl2ga  3549  vtocl3ga  3552  vtoclri  3556  disjxiun  5108  wfis3  6359  opabiota  6964  fvmpt3  6995  fvmptss  7003  fnressn  7156  fressnfv  7158  caovord  7622  caovmo  7648  ordunisuc  7828  tfis3  7854  fpr2a  8299  frrdmcl  8305  onfununi  8328  smogt  8354  tz7.44-1  8393  tz7.44-2  8394  tz7.44-3  8395  nnacl  8597  nnmcl  8598  nnecl  8599  nnacom  8603  nnaass  8608  nndi  8609  nnmass  8610  nnmsucr  8611  nnmcom  8612  nnmordi  8617  ixpfn  8901  findcard  9148  findcard2  9149  marypha1  9394  cantnfle  9640  cantnflem1  9658  cnfcom  9669  frr2  9732  fseqenlem1  10008  nnadju  10181  ackbij1lem8  10209  cardcf  10235  cfsmolem  10254  wunex2  10723  ingru  10800  recrecnq  10952  prlem934  11018  nn1suc  12255  uzind4s2  12933  rpnnen1lem6  13006  cnref1o  13009  xmulasslem  13311  om2uzsuci  13984  expcl2lem  14109  hashpw  14473  seqcoll  14501  climub  15713  climserle  15714  sumrblem  15762  fsumcvg  15763  summolem2a  15766  infcvgaux2i  15912  prodfn0  15948  prodfrec  15949  prodrblem  15983  fprodcvg  15984  prodmolem2a  15988  divalglem8  16458  bezoutlem1  16597  alginv  16633  algcvg  16634  algcvga  16637  algfx  16638  prmind2  16743  prmpwdvds  16964  cnextfvval  24191  xrsxmet  24936  xrhmeo  25074  cmetcaulem  25416  bcth3  25459  itg2addlem  25886  taylfval  26488  sinord  26665  logexprlim  27355  lgsdir2lem4  27458  noseqind  28451  hlim2  31485  elnlfn  32221  lnconi  32326  chirredlem3  32685  chirredlem4  32686  cnre2csqlem  34245  eulerpartlemsf  34694  eulerpartlemn  34716  bnj1321  35360  bnj1418  35373  subfacp1lem1  35604  nn0prpwlem  36756  findreccl  36887  weiunlem  36897  mptsnunlem  37907  rdgeqoa  37939  domalom  37973  poimirlem22  38216  poimirlem26  38220  mblfinlem3  38233  mblfinlem4  38234  ismblfin  38235  ftc1anclem3  38269  ftc1anclem8  38274  sdclem2  38316  iscringd  38572  renegclALT  39662  zindbi  43600  fmuldfeq  46226  sumnnodd  46273  iblspltprt  46614  stoweidlem2  46643  stoweidlem17  46658  stoweidlem21  46662  stoweidlem43  46684  stoweidlem51  46692  wallispi  46711