Theorem vtoclga 3566

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  vtocl2ga  3567  vtoclri  3577  disjxiun  5145  wfis3  6360  opabiota  6972  fvmpt3  7000  fvmptss  7008  fnressn  7153  fressnfv  7155  caovord  7615  caovmo  7641  ordunisuc  7817  tfis3  7844  fpr2a  8284  frrdmcl  8290  wfr2aOLD  8323  onfununi  8338  smogt  8364  tz7.44-1  8403  tz7.44-2  8404  tz7.44-3  8405  nnacl  8608  nnmcl  8609  nnecl  8610  nnacom  8614  nnaass  8619  nndi  8620  nnmass  8621  nnmsucr  8622  nnmcom  8623  nnmordi  8628  ixpfn  8894  findcard  9160  findcard2  9161  findcard2OLD  9281  marypha1  9426  cantnfle  9663  cantnflem1  9681  cnfcom  9692  frr2  9752  fseqenlem1  10016  nnadju  10189  ackbij1lem8  10219  cardcf  10244  cfsmolem  10262  wunex2  10730  ingru  10807  recrecnq  10959  prlem934  11025  nn1suc  12231  uzind4s2  12890  rpnnen1lem6  12963  cnref1o  12966  xmulasslem  13261  om2uzsuci  13910  expcl2lem  14036  hashpw  14393  seqcoll  14422  climub  15605  climserle  15606  sumrblem  15654  fsumcvg  15655  summolem2a  15658  infcvgaux2i  15801  prodfn0  15837  prodfrec  15838  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  divalglem8  16340  bezoutlem1  16478  alginv  16509  algcvg  16510  algcvga  16513  algfx  16514  prmind2  16619  prmpwdvds  16834  cnextfvval  23561  xrsxmet  24317  xrhmeo  24454  cmetcaulem  24797  bcth3  24840  itg2addlem  25268  taylfval  25863  sinord  26035  logexprlim  26718  lgsdir2lem4  26821  hlim2  30433  elnlfn  31169  lnconi  31274  chirredlem3  31633  chirredlem4  31634  cnre2csqlem  32879  eulerpartlemsf  33347  eulerpartlemn  33369  bnj1321  34027  bnj1418  34040  subfacp1lem1  34159  nn0prpwlem  35196  findreccl  35327  mptsnunlem  36208  rdgeqoa  36240  domalom  36274  poimirlem22  36499  poimirlem26  36503  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  ftc1anclem3  36552  ftc1anclem8  36557  sdclem2  36599  iscringd  36855  renegclALT  37822  zindbi  41671  fmuldfeq  44286  sumnnodd  44333  iblspltprt  44676  stoweidlem2  44705  stoweidlem17  44720  stoweidlem21  44724  stoweidlem43  44746  stoweidlem51  44754  wallispi  44773  upwordisword  45582