Theorem vtoclg 3566

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2178. (Revised by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)

Hypotheses

Ref	Expression
vtoclg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclg.2	⊢ 𝜑

Assertion

Ref	Expression
vtoclg	⊢ (𝐴 ∈ 𝑉 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		vtoclg.2	. . 3 ⊢ 𝜑
2		vtoclg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	mpbii 233	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4	3	vtocleg 3565	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  vtoclbg  3569  vtocl2g  3586  vtocl3g  3587  vtoclga  3589  nelrdva  3727  moeq3  3734  mo2icl  3736  sbcim1  3861  sbctt  3880  csbconstg  3940  sbcnestgfw  4444  sbcnestgf  4449  csbun  4464  csbin  4465  csbdif  4547  csbif  4605  axrep6g  5311  inex1g  5337  ssexg  5341  pwexg  5396  prex  5452  sels  5458  opth  5496  csbopab  5574  csbopabgALT  5575  vtoclr  5763  resieq  6020  csbima12  6108  dmsnsnsn  6251  csbcog  6328  dfpred3g  6344  preddowncl  6364  ordelord  6417  iota5  6556  csbiota  6566  funmoOLD  6594  funimaexgOLD  6665  fconstg  6808  funbrfv  6971  fvelimab  6994  ssimaexg  7008  fvelrn  7110  isoselem  7377  csbriota  7420  csbov123  7492  ovg  7615  caovmo  7687  uniexg  7775  fnse  8174  onfununi  8397  rdg0g  8483  ensn1g  9084  fundmeng  9097  xpdom2g  9134  canth2g  9197  ssfi  9240  php2OLD  9286  canthwdom  9648  zfregcl  9663  elirr  9666  ttrclselem2  9795  tcvalg  9807  tz9.13g  9861  rankvalg  9886  ranklim  9913  r1pwALT  9915  rankuni2b  9922  rankuni  9932  cfslb2n  10337  itunitc1  10489  itunitc  10490  ituniiun  10491  hsmex  10501  axdc2lem  10517  ac7g  10543  ac6sg  10557  numthcor  10563  weth  10564  rankcf  10846  nqereu  10998  prnmax  11064  prlem936  11116  ltord1  11816  xmulasslem  13347  axdc4uz  14035  relexpind  15113  climshft  15622  telfsumo  15850  fsumparts  15854  lcmgcdlem  16653  mreacs  17716  dprdval  20047  fiinopn  22928  neiptoptop  23160  neiptopnei  23161  pt1hmeo  23835  isfildlem  23886  alexsublem  24073  ustuqtop4  24274  voliunlem3  25606  dvbsss  25957  dvfsumlem2  26087  dvfsumlem2OLD  26088  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  carsgsigalem  34280  carsgclctunlem2  34284  carsgclctun  34286  pmeasmono  34289  pmeasadd  34290  sitgclg  34307  mclsrcl  35529  iota5f  35686  shftvalg  35694  dfrdg2  35759  fvsingle  35884  fullfunfv  35911  ranksng  36131  rankelg  36132  rankpwg  36133  rankeq1o  36135  bj-adjg1  37009  mblfinlem3  37619  ismrer1  37798  mzpclall  42683  mzpcompact2  42708  diophrw  42715  monotuz  42898  monotoddzz  42900  oddcomabszz  42901  flcidc  43131  nzss  44286  pm14.122b  44392  sbiota1  44403  fiiuncl  44967  axccdom  45129  axccd  45136  monoords  45212  fperiodmullem  45218  0ellimcdiv  45570  cncfperiod  45800  icccncfext  45808  fperdvper  45840  dvnmul  45864  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem4  45925  stoweidlem6  45927  stoweidlem8  45929  stoweidlem15  45936  stoweidlem16  45937  stoweidlem19  45940  stoweidlem20  45941  stoweidlem22  45943  stoweidlem23  45944  stoweidlem27  45948  stoweidlem30  45951  stoweidlem32  45953  stoweidlem34  45955  stoweidlem42  45963  stoweidlem48  45969  fourierdlem11  46039  fourierdlem16  46044  fourierdlem21  46049  fourierdlem41  46069  fourierdlem42  46070  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem68  46095  fourierdlem72  46099  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  sge0f1o  46303  sge0p1  46335  hoidmvlelem4  46519  smfpimcclem  46728  funressnmo  46961  aiota0def  47011  csbafv12g  47052  csbaovg  47095  csbafv212g  47134  funressndmafv2rn  47138  funressnbrafv2  47159  funbrafv2  47162