Theorem vtoclg 3481

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

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∃wex 1787   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-clel 2816

This theorem is referenced by:  vtoclbg  3483  vtocl2g  3486  vtocl3g  3487  vtoclga  3489  nelrdva  3618  moeq3  3625  mo2icl  3627  sbcim1  3750  sbctt  3771  csbconstg  3830  sbcnestgfw  4333  sbcnestgf  4338  csbun  4353  csbin  4354  csbif  4496  inex1g  5212  ssexg  5216  pwexg  5271  snex  5324  prex  5325  opth  5360  csbopab  5436  csbopabgALT  5437  vtoclr  5612  resieq  5862  csbima12  5947  dmsnsnsn  6083  dfpred3g  6171  predbrg  6182  preddowncl  6190  ordelord  6235  iota5  6363  csbiota  6373  funmo  6396  funimaexg  6466  fconstg  6606  funbrfv  6763  fvelimab  6784  ssimaexg  6797  fvelrn  6897  isoselem  7150  csbriota  7186  csbov123  7255  ovg  7373  caovmo  7445  uniexg  7528  fnse  7900  onfununi  8078  rdg0g  8163  ensn1g  8696  fundmeng  8709  xpdom2g  8741  canth2g  8800  php2  8831  ssfi  8851  canthwdom  9195  zfregcl  9210  elirr  9213  tcvalg  9354  tz9.13g  9408  rankvalg  9433  ranklim  9460  r1pwALT  9462  rankuni2b  9469  rankuni  9479  cfslb2n  9882  itunitc1  10034  itunitc  10035  ituniiun  10036  hsmex  10046  axdc2lem  10062  ac7g  10088  ac6sg  10102  numthcor  10108  weth  10109  pwfseqlem4  10276  rankcf  10391  nqereu  10543  prnmax  10609  prlem936  10661  ltord1  11358  xmulasslem  12875  axdc4uz  13557  relexpind  14627  climshft  15137  telfsumo  15366  fsumparts  15370  lcmgcdlem  16163  mreacs  17161  dprdval  19390  fiinopn  21798  neiptoptop  22028  neiptopnei  22029  pt1hmeo  22703  isfildlem  22754  alexsublem  22941  ustuqtop4  23142  voliunlem3  24449  dvbsss  24799  dvfsumlem2  24924  acunirnmpt  30716  acunirnmpt2  30717  acunirnmpt2f  30718  carsgsigalem  31994  carsgclctunlem2  31998  carsgclctun  32000  pmeasmono  32003  pmeasadd  32004  sitgclg  32021  mclsrcl  33236  iota5f  33384  shftvalg  33415  dfrdg2  33490  fvsingle  33959  fullfunfv  33986  ranksng  34206  rankelg  34207  rankpwg  34208  rankeq1o  34210  csbdif  35233  mblfinlem3  35553  ismrer1  35733  mzpclall  40252  mzpcompact2  40277  diophrw  40284  monotuz  40466  monotoddzz  40468  oddcomabszz  40469  flcidc  40702  csbcog  40934  nzss  41608  pm14.122b  41714  sbiota1  41725  fiiuncl  42286  axccdom  42435  axccd  42441  monoords  42509  fperiodmullem  42515  0ellimcdiv  42865  cncfperiod  43095  icccncfext  43103  fperdvper  43135  dvnmul  43159  dvnprodlem2  43163  iblspltprt  43189  itgspltprt  43195  stoweidlem4  43220  stoweidlem6  43222  stoweidlem8  43224  stoweidlem15  43231  stoweidlem16  43232  stoweidlem19  43235  stoweidlem20  43236  stoweidlem22  43238  stoweidlem23  43239  stoweidlem27  43243  stoweidlem30  43246  stoweidlem32  43248  stoweidlem34  43250  stoweidlem42  43258  stoweidlem48  43264  fourierdlem11  43334  fourierdlem16  43339  fourierdlem21  43344  fourierdlem41  43364  fourierdlem42  43365  fourierdlem46  43368  fourierdlem48  43370  fourierdlem49  43371  fourierdlem50  43372  fourierdlem68  43390  fourierdlem72  43394  fourierdlem76  43398  fourierdlem79  43401  fourierdlem81  43403  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem92  43414  fourierdlem97  43419  fourierdlem103  43425  fourierdlem104  43426  fourierdlem111  43433  sge0f1o  43595  sge0p1  43627  hoidmvlelem4  43811  smfpimcclem  44012  funressnmo  44212  aiota0def  44260  csbafv12g  44301  csbaovg  44344  csbafv212g  44383  funressndmafv2rn  44387  funressnbrafv2  44408  funbrafv2  44411