Theorem vtoclga 3543

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839

This theorem is referenced by:  vtocl2ga  3544  vtocl3ga  3547  vtoclri  3551  disjxiun  5099  wfis3  6346  opabiota  6951  fvmpt3  6982  fvmptss  6990  fnressn  7143  fressnfv  7145  caovord  7609  caovmo  7635  ordunisuc  7814  tfis3  7840  fpr2a  8285  frrdmcl  8291  onfununi  8314  smogt  8340  tz7.44-1  8379  tz7.44-2  8380  tz7.44-3  8381  nnacl  8583  nnmcl  8584  nnecl  8585  nnacom  8589  nnaass  8594  nndi  8595  nnmass  8596  nnmsucr  8597  nnmcom  8598  nnmordi  8603  ixpfn  8887  findcard  9134  findcard2  9135  marypha1  9382  cantnfle  9628  cantnflem1  9646  cnfcom  9657  frr2  9720  fseqenlem1  9982  nnadju  10156  ackbij1lem8  10184  cardcf  10210  cfsmolem  10229  wunex2  10698  ingru  10775  recrecnq  10927  prlem934  10993  nn1suc  12234  uzind4s2  12912  rpnnen1lem6  12985  cnref1o  12988  xmulasslem  13290  om2uzsuci  13963  expcl2lem  14088  hashpw  14451  seqcoll  14479  climub  15691  climserle  15692  sumrblem  15740  fsumcvg  15741  summolem2a  15744  infcvgaux2i  15890  prodfn0  15926  prodfrec  15927  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  divalglem8  16436  bezoutlem1  16575  alginv  16611  algcvg  16612  algcvga  16615  algfx  16616  prmind2  16721  prmpwdvds  16942  cnextfvval  24127  xrsxmet  24872  xrhmeo  25010  cmetcaulem  25352  bcth3  25395  itg2addlem  25822  taylfval  26424  sinord  26601  logexprlim  27291  lgsdir2lem4  27394  noseqind  28387  hlim2  31397  elnlfn  32133  lnconi  32238  chirredlem3  32597  chirredlem4  32598  cnre2csqlem  34209  eulerpartlemsf  34658  eulerpartlemn  34680  bnj1321  35324  bnj1418  35337  subfacp1lem1  35534  nn0prpwlem  36687  findreccl  36818  weiunlem  36828  mptsnunlem  37837  rdgeqoa  37869  domalom  37903  poimirlem22  38146  poimirlem26  38150  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  ftc1anclem3  38199  ftc1anclem8  38204  sdclem2  38246  iscringd  38502  renegclALT  39592  zindbi  43528  fmuldfeq  46164  sumnnodd  46211  iblspltprt  46552  stoweidlem2  46581  stoweidlem17  46596  stoweidlem21  46600  stoweidlem43  46622  stoweidlem51  46630  wallispi  46649