Theorem vtoclga 3531

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 2823	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3510	. 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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810

This theorem is referenced by:  vtocl2ga  3532  vtocl3ga  3537  vtoclri  3543  disjxiun  5094  wfis3  6314  opabiota  6915  fvmpt3  6945  fvmptss  6953  fnressn  7103  fressnfv  7105  caovord  7569  caovmo  7595  ordunisuc  7774  tfis3  7800  fpr2a  8244  frrdmcl  8250  onfununi  8273  smogt  8299  tz7.44-1  8337  tz7.44-2  8338  tz7.44-3  8339  nnacl  8539  nnmcl  8540  nnecl  8541  nnacom  8545  nnaass  8550  nndi  8551  nnmass  8552  nnmsucr  8553  nnmcom  8554  nnmordi  8559  ixpfn  8843  findcard  9090  findcard2  9091  marypha1  9339  cantnfle  9582  cantnflem1  9600  cnfcom  9611  frr2  9674  fseqenlem1  9936  nnadju  10110  ackbij1lem8  10138  cardcf  10164  cfsmolem  10182  wunex2  10651  ingru  10728  recrecnq  10880  prlem934  10946  nn1suc  12169  uzind4s2  12824  rpnnen1lem6  12897  cnref1o  12900  xmulasslem  13202  om2uzsuci  13873  expcl2lem  13998  hashpw  14361  seqcoll  14389  climub  15587  climserle  15588  sumrblem  15636  fsumcvg  15637  summolem2a  15640  infcvgaux2i  15783  prodfn0  15819  prodfrec  15820  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  divalglem8  16329  bezoutlem1  16468  alginv  16504  algcvg  16505  algcvga  16508  algfx  16509  prmind2  16614  prmpwdvds  16834  cnextfvval  24011  xrsxmet  24756  xrhmeo  24902  cmetcaulem  25246  bcth3  25289  itg2addlem  25717  taylfval  26324  sinord  26501  logexprlim  27194  lgsdir2lem4  27297  noseqind  28271  hlim2  31248  elnlfn  31984  lnconi  32089  chirredlem3  32448  chirredlem4  32449  cnre2csqlem  34046  eulerpartlemsf  34495  eulerpartlemn  34517  bnj1321  35162  bnj1418  35175  subfacp1lem1  35352  nn0prpwlem  36495  findreccl  36626  weiunlem2  36636  mptsnunlem  37512  rdgeqoa  37544  domalom  37578  poimirlem22  37812  poimirlem26  37816  mblfinlem3  37829  mblfinlem4  37830  ismblfin  37831  ftc1anclem3  37865  ftc1anclem8  37870  sdclem2  37912  iscringd  38168  renegclALT  39258  zindbi  43225  fmuldfeq  45866  sumnnodd  45913  iblspltprt  46254  stoweidlem2  46283  stoweidlem17  46298  stoweidlem21  46302  stoweidlem43  46324  stoweidlem51  46332  wallispi  46351