Theorem vtoclg 3505

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2171. (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

Step	Hyp	Ref	Expression
1		elisset 2820	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg.2	. . . 4 ⊢ 𝜑
3		vtoclg.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	2, 3	mpbii 232	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
5	4	exlimiv 1933	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
6	1, 5	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1782   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-clel 2816

This theorem is referenced by:  vtoclbg  3507  vtocl2g  3510  vtocl3g  3511  vtoclga  3513  nelrdva  3640  moeq3  3647  mo2icl  3649  sbcim1  3772  sbctt  3792  csbconstg  3851  sbcnestgfw  4352  sbcnestgf  4357  csbun  4372  csbin  4373  csbdif  4458  csbif  4516  axrep6g  5217  inex1g  5243  ssexg  5247  pwexg  5301  snex  5354  prex  5355  opth  5391  csbopab  5468  csbopabgALT  5469  vtoclr  5650  resieq  5902  csbima12  5987  dmsnsnsn  6123  csbcog  6200  dfpred3g  6214  predbrg  6224  preddowncl  6235  ordelord  6288  iota5  6416  csbiota  6426  funmo  6450  funimaexg  6520  fconstg  6661  funbrfv  6820  fvelimab  6841  ssimaexg  6854  fvelrn  6954  isoselem  7212  csbriota  7248  csbov123  7317  ovg  7437  caovmo  7509  uniexg  7593  fnse  7974  onfununi  8172  rdg0g  8258  ensn1g  8809  fundmeng  8822  xpdom2g  8855  canth2g  8918  ssfi  8956  php2OLD  9006  canthwdom  9338  zfregcl  9353  elirr  9356  ttrclselem2  9484  tcvalg  9496  tz9.13g  9550  rankvalg  9575  ranklim  9602  r1pwALT  9604  rankuni2b  9611  rankuni  9621  cfslb2n  10024  itunitc1  10176  itunitc  10177  ituniiun  10178  hsmex  10188  axdc2lem  10204  ac7g  10230  ac6sg  10244  numthcor  10250  weth  10251  pwfseqlem4  10418  rankcf  10533  nqereu  10685  prnmax  10751  prlem936  10803  ltord1  11501  xmulasslem  13019  axdc4uz  13704  relexpind  14775  climshft  15285  telfsumo  15514  fsumparts  15518  lcmgcdlem  16311  mreacs  17367  dprdval  19606  fiinopn  22050  neiptoptop  22282  neiptopnei  22283  pt1hmeo  22957  isfildlem  23008  alexsublem  23195  ustuqtop4  23396  voliunlem3  24716  dvbsss  25066  dvfsumlem2  25191  acunirnmpt  30996  acunirnmpt2  30997  acunirnmpt2f  30998  carsgsigalem  32282  carsgclctunlem2  32286  carsgclctun  32288  pmeasmono  32291  pmeasadd  32292  sitgclg  32309  mclsrcl  33523  iota5f  33669  shftvalg  33697  dfrdg2  33771  fvsingle  34222  fullfunfv  34249  ranksng  34469  rankelg  34470  rankpwg  34471  rankeq1o  34473  mblfinlem3  35816  ismrer1  35996  mzpclall  40549  mzpcompact2  40574  diophrw  40581  monotuz  40763  monotoddzz  40765  oddcomabszz  40766  flcidc  40999  nzss  41935  pm14.122b  42041  sbiota1  42052  fiiuncl  42613  axccdom  42762  axccd  42768  monoords  42836  fperiodmullem  42842  0ellimcdiv  43190  cncfperiod  43420  icccncfext  43428  fperdvper  43460  dvnmul  43484  dvnprodlem2  43488  iblspltprt  43514  itgspltprt  43520  stoweidlem4  43545  stoweidlem6  43547  stoweidlem8  43549  stoweidlem15  43556  stoweidlem16  43557  stoweidlem19  43560  stoweidlem20  43561  stoweidlem22  43563  stoweidlem23  43564  stoweidlem27  43568  stoweidlem30  43571  stoweidlem32  43573  stoweidlem34  43575  stoweidlem42  43583  stoweidlem48  43589  fourierdlem11  43659  fourierdlem16  43664  fourierdlem21  43669  fourierdlem41  43689  fourierdlem42  43690  fourierdlem46  43693  fourierdlem48  43695  fourierdlem49  43696  fourierdlem50  43697  fourierdlem68  43715  fourierdlem72  43719  fourierdlem76  43723  fourierdlem79  43726  fourierdlem81  43728  fourierdlem89  43736  fourierdlem90  43737  fourierdlem91  43738  fourierdlem92  43739  fourierdlem97  43744  fourierdlem103  43750  fourierdlem104  43751  fourierdlem111  43758  sge0f1o  43920  sge0p1  43952  hoidmvlelem4  44136  smfpimcclem  44340  funressnmo  44540  aiota0def  44588  csbafv12g  44629  csbaovg  44672  csbafv212g  44711  funressndmafv2rn  44715  funressnbrafv2  44736  funbrafv2  44739