Theorem vtoclga 3536

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 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3517	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 53	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  vtocl2ga  3537  vtocl3ga  3540  vtoclri  3544  disjxiun  5099  wfis3  6360  opabiota  6967  fvmpt3  6998  fvmptss  7006  fnressn  7162  fressnfv  7164  caovord  7632  caovmo  7658  ordunisuc  7843  tfis3  7869  fpr2a  8320  frrdmcl  8326  onfununi  8349  smogt  8375  tz7.44-1  8414  tz7.44-2  8415  tz7.44-3  8416  nnacl  8620  nnmcl  8621  nnecl  8622  nnacom  8626  nnaass  8631  nndi  8632  nnmass  8633  nnmsucr  8634  nnmcom  8635  nnmordi  8640  ixpfn  8931  findcard  9179  findcard2  9180  marypha1  9426  cantnfle  9672  cantnflem1  9690  cnfcom  9701  frr2  9764  fseqenlem1  10103  nnadju  10276  ackbij1lem8  10304  cardcf  10329  cfsmolem  10348  wunex2  10823  ingru  10900  recrecnq  11052  prlem934  11118  nn1suc  12357  uzind4s2  13036  rpnnen1lem6  13110  cnref1o  13113  xmulasslem  13415  om2uzsuci  14091  expcl2lem  14216  hashpw  14581  seqcoll  14609  climub  15829  climserle  15830  sumrblem  15877  fsumcvg  15878  summolem2a  15881  infcvgaux2i  16027  prodfn0  16063  prodfrec  16064  prodrblem  16096  fprodcvg  16097  prodmolem2a  16101  divalglem8  16570  bezoutlem1  16712  alginv  16750  algcvg  16751  algcvga  16754  algfx  16755  prmind2  16860  prmpwdvds  17082  cnextfvval  24384  xrsxmet  25129  xrhmeo  25267  cmetcaulem  25609  bcth3  25652  itg2addlem  26079  taylfval  26686  sinord  26862  logexprlim  27552  lgsdir2lem4  27655  noseqind  28678  hlim2  31794  elnlfn  32530  lnconi  32635  chirredlem3  32994  chirredlem4  32995  cnre2csqlem  34542  eulerpartlemsf  34991  eulerpartlemn  35013  bnj1321  35657  bnj1418  35670  subfacp1lem1  35944  nn0prpwlem  37110  findreccl  37241  weiunlem  37251  mptsnunlem  38262  rdgeqoa  38294  domalom  38328  poimirlem22  38561  poimirlem26  38565  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  ftc1anclem3  38614  ftc1anclem8  38619  sdclem2  38677  iscringd  38933  renegclALT  40021  zindbi  43953  fmuldfeq  46595  sumnnodd  46642  iblspltprt  46983  stoweidlem2  47012  stoweidlem17  47027  stoweidlem21  47031  stoweidlem43  47053  stoweidlem51  47061  wallispi  47080