Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclg Structured version   Visualization version   GIF version

Theorem vtoclg 3516
 Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2175. (Revised by SN, 20-Apr-2024.)
Hypotheses
Ref Expression
vtoclg.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclg.2 𝜑
Assertion
Ref Expression
vtoclg (𝐴𝑉𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg
StepHypRef Expression
1 elisset 3453 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg.2 . . . 4 𝜑
3 vtoclg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
42, 3mpbii 236 . . 3 (𝑥 = 𝐴𝜓)
54exlimiv 1931 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
61, 5syl 17 1 (𝐴𝑉𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  vtoclbg  3518  vtocl2g  3521  vtoclga  3523  nelrdva  3646  moeq3  3653  mo2icl  3655  sbctt  3792  csb0  4317  sbcnestgfw  4329  sbcnestgf  4334  csbun  4349  csbin  4350  csbif  4483  inex1g  5191  ssexg  5195  pwexg  5248  snex  5301  prex  5302  opth  5337  csbopab  5411  csbopabgALT  5412  vtoclr  5583  resieq  5833  csbima12  5918  dmsnsnsn  6048  dfpred3g  6134  predbrg  6143  preddowncl  6150  ordelord  6188  iota5  6315  csbiota  6325  funmo  6348  funimaexg  6418  fconstg  6548  funbrfv  6701  fvelimab  6722  ssimaexg  6734  fvelrn  6831  isoselem  7083  csbriota  7118  csbov123  7187  ovg  7304  caovmo  7376  uniexg  7459  fnse  7823  onfununi  7979  rdg0g  8064  ensn1g  8575  fundmeng  8585  xpdom2g  8614  canth2g  8673  php2  8704  canthwdom  9045  zfregcl  9060  elirr  9063  tcvalg  9182  tz9.13g  9223  rankvalg  9248  ranklim  9275  r1pwALT  9277  rankuni2b  9284  rankuni  9294  cfslb2n  9697  itunitc1  9849  itunitc  9850  ituniiun  9851  hsmex  9861  axdc2lem  9877  ac7g  9903  ac6sg  9917  numthcor  9923  weth  9924  pwfseqlem4  10091  rankcf  10206  nqereu  10358  prnmax  10424  prlem936  10476  ltord1  11173  xmulasslem  12686  axdc4uz  13367  relexpind  14435  climshft  14945  telfsumo  15169  fsumparts  15173  lcmgcdlem  15960  mreacs  16941  dprdval  19139  fiinopn  21547  neiptoptop  21777  neiptopnei  21778  pt1hmeo  22452  isfildlem  22503  alexsublem  22690  ustuqtop4  22891  voliunlem3  24197  dvbsss  24546  dvfsumlem2  24671  acunirnmpt  30466  acunirnmpt2  30467  acunirnmpt2f  30468  carsgsigalem  31749  carsgclctunlem2  31753  carsgclctun  31755  pmeasmono  31758  pmeasadd  31759  sitgclg  31776  mclsrcl  32987  iota5f  33135  shftvalg  33146  dfrdg2  33223  fvsingle  33641  fullfunfv  33668  ranksng  33888  rankelg  33889  rankpwg  33890  rankeq1o  33892  csbdif  34893  mblfinlem3  35247  ismrer1  35427  mzpclall  39839  mzpcompact2  39864  diophrw  39871  monotuz  40053  monotoddzz  40055  oddcomabszz  40056  flcidc  40289  csbcog  40521  nzss  41192  pm14.122b  41298  sbiota1  41309  fiiuncl  41870  axccdom  42021  axccd  42029  monoords  42097  fperiodmullem  42103  0ellimcdiv  42459  cncfperiod  42689  icccncfext  42697  fperdvper  42729  dvnmul  42753  dvnprodlem2  42757  iblspltprt  42783  itgspltprt  42789  stoweidlem4  42814  stoweidlem6  42816  stoweidlem8  42818  stoweidlem15  42825  stoweidlem16  42826  stoweidlem19  42829  stoweidlem20  42830  stoweidlem22  42832  stoweidlem23  42833  stoweidlem27  42837  stoweidlem30  42840  stoweidlem32  42842  stoweidlem34  42844  stoweidlem42  42852  stoweidlem48  42858  fourierdlem11  42928  fourierdlem16  42933  fourierdlem21  42938  fourierdlem41  42958  fourierdlem42  42959  fourierdlem46  42962  fourierdlem48  42964  fourierdlem49  42965  fourierdlem50  42966  fourierdlem68  42984  fourierdlem72  42988  fourierdlem76  42992  fourierdlem79  42995  fourierdlem81  42997  fourierdlem89  43005  fourierdlem90  43006  fourierdlem91  43007  fourierdlem92  43008  fourierdlem97  43013  fourierdlem103  43019  fourierdlem104  43020  fourierdlem111  43027  sge0f1o  43189  sge0p1  43221  hoidmvlelem4  43405  smfpimcclem  43606  funressnmo  43806  aiota0def  43819  csbafv12g  43861  csbaovg  43904  csbafv212g  43943  funressndmafv2rn  43947  funressnbrafv2  43968  funbrafv2  43971
 Copyright terms: Public domain W3C validator