Theorem vtoclg 3509

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 3508	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  vtoclbg  3512  vtocl2g  3529  vtocl3g  3530  vtoclga  3532  nelrdva  3665  moeq3  3672  mo2icl  3674  sbcim1  3796  sbctt  3812  csbconstg  3870  sbcnestgfw  4372  sbcnestgf  4377  csbun  4392  csbin  4393  csbdif  4475  csbif  4534  axrep6g  5229  inex1g  5258  ssexg  5262  pwexg  5317  prex  5376  sels  5382  opth  5419  csbopab  5498  csbopabgALT  5499  vtoclr  5682  resieq  5941  csbima12  6030  dmsnsnsn  6169  csbcog  6245  dfpred3g  6261  preddowncl  6280  ordelord  6329  iota5  6465  csbiota  6475  fconstg  6711  funbrfv  6871  fvelimab  6895  ssimaexg  6909  fvelrn  7010  isoselem  7278  csbriota  7321  csbov123  7393  ovg  7514  caovmo  7586  uniexg  7676  fnse  8066  onfununi  8264  rdg0g  8349  ensn1g  8947  fundmeng  8957  xpdom2g  8990  canth2g  9048  ssfi  9087  canthwdom  9471  zfregcl  9486  zfregclOLD  9487  elirr  9491  ttrclselem2  9622  tcvalg  9634  tz9.13g  9688  rankvalg  9713  ranklim  9740  r1pwALT  9742  rankuni2b  9749  rankuni  9759  cfslb2n  10162  itunitc1  10314  itunitc  10315  ituniiun  10316  hsmex  10326  axdc2lem  10342  ac7g  10368  ac6sg  10382  numthcor  10388  weth  10389  rankcf  10671  nqereu  10823  prnmax  10889  prlem936  10941  ltord1  11646  xmulasslem  13187  axdc4uz  13891  relexpind  14971  climshft  15483  telfsumo  15709  fsumparts  15713  lcmgcdlem  16517  mreacs  17564  dprdval  19884  fiinopn  22786  neiptoptop  23016  neiptopnei  23017  pt1hmeo  23691  isfildlem  23742  alexsublem  23929  ustuqtop4  24130  voliunlem3  25451  dvbsss  25801  dvfsumlem2  25931  dvfsumlem2OLD  25932  acunirnmpt  32603  acunirnmpt2  32604  acunirnmpt2f  32605  carsgsigalem  34289  carsgclctunlem2  34293  carsgclctun  34295  pmeasmono  34298  pmeasadd  34299  sitgclg  34316  mclsrcl  35544  iota5f  35707  shftvalg  35715  dfrdg2  35779  fvsingle  35904  fullfunfv  35931  ranksng  36151  rankelg  36152  rankpwg  36153  rankeq1o  36155  bj-adjg1  37027  mblfinlem3  37649  ismrer1  37828  mzpclall  42710  mzpcompact2  42735  diophrw  42742  monotuz  42924  monotoddzz  42926  oddcomabszz  42927  flcidc  43153  nzss  44300  pm14.122b  44406  sbiota1  44417  fiiuncl  45053  axccdom  45210  axccd  45217  monoords  45289  fperiodmullem  45295  0ellimcdiv  45640  cncfperiod  45870  icccncfext  45878  fperdvper  45910  dvnmul  45934  dvnprodlem2  45938  iblspltprt  45964  itgspltprt  45970  stoweidlem4  45995  stoweidlem6  45997  stoweidlem8  45999  stoweidlem15  46006  stoweidlem16  46007  stoweidlem19  46010  stoweidlem20  46011  stoweidlem22  46013  stoweidlem23  46014  stoweidlem27  46018  stoweidlem30  46021  stoweidlem32  46023  stoweidlem34  46025  stoweidlem42  46033  stoweidlem48  46039  fourierdlem11  46109  fourierdlem16  46114  fourierdlem21  46119  fourierdlem41  46139  fourierdlem42  46140  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem68  46165  fourierdlem72  46169  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem92  46189  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  sge0f1o  46373  sge0p1  46405  hoidmvlelem4  46589  smfpimcclem  46798  funressnmo  47040  aiota0def  47090  csbafv12g  47131  csbaovg  47174  csbafv212g  47213  funressndmafv2rn  47217  funressnbrafv2  47238  funbrafv2  47241