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  32610  acunirnmpt2  32611  acunirnmpt2f  32612  carsgsigalem  34299  carsgclctunlem2  34303  carsgclctun  34305  pmeasmono  34308  pmeasadd  34309  sitgclg  34326  mclsrcl  35554  iota5f  35717  shftvalg  35725  dfrdg2  35789  fvsingle  35914  fullfunfv  35941  ranksng  36161  rankelg  36162  rankpwg  36163  rankeq1o  36165  bj-adjg1  37037  mblfinlem3  37659  ismrer1  37838  mzpclall  42720  mzpcompact2  42745  diophrw  42752  monotuz  42934  monotoddzz  42936  oddcomabszz  42937  flcidc  43163  nzss  44310  pm14.122b  44416  sbiota1  44427  fiiuncl  45063  axccdom  45220  axccd  45227  monoords  45299  fperiodmullem  45305  0ellimcdiv  45650  cncfperiod  45880  icccncfext  45888  fperdvper  45920  dvnmul  45944  dvnprodlem2  45948  iblspltprt  45974  itgspltprt  45980  stoweidlem4  46005  stoweidlem6  46007  stoweidlem8  46009  stoweidlem15  46016  stoweidlem16  46017  stoweidlem19  46020  stoweidlem20  46021  stoweidlem22  46023  stoweidlem23  46024  stoweidlem27  46028  stoweidlem30  46031  stoweidlem32  46033  stoweidlem34  46035  stoweidlem42  46043  stoweidlem48  46049  fourierdlem11  46119  fourierdlem16  46124  fourierdlem21  46129  fourierdlem41  46149  fourierdlem42  46150  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem50  46157  fourierdlem68  46175  fourierdlem72  46179  fourierdlem76  46183  fourierdlem79  46186  fourierdlem81  46188  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem92  46199  fourierdlem97  46204  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  sge0f1o  46383  sge0p1  46415  hoidmvlelem4  46599  smfpimcclem  46808  funressnmo  47050  aiota0def  47100  csbafv12g  47141  csbaovg  47184  csbafv212g  47223  funressndmafv2rn  47227  funressnbrafv2  47248  funbrafv2  47251