Theorem vtoclg 3514

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2170. (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 2818	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		vtoclg.2	. . . 4 ⊢ 𝜑
3		vtoclg.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	2, 3	mpbii 232	. . 3 ⊢ (𝑥 = 𝐴 → 𝜓)
5	4	exlimiv 1932	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
6	1, 5	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ∃wex 1780   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-clel 2814

This theorem is referenced by:  vtoclbg  3516  vtocl2g  3519  vtocl3g  3520  vtoclga  3522  nelrdva  3650  moeq3  3657  mo2icl  3659  sbcim1  3782  sbctt  3802  csbconstg  3861  sbcnestgfw  4364  sbcnestgf  4369  csbun  4384  csbin  4385  csbdif  4471  csbif  4529  axrep6g  5234  inex1g  5260  ssexg  5264  pwexg  5318  snexg  5372  prex  5374  sels  5380  opth  5415  csbopab  5493  csbopabgALT  5494  vtoclr  5675  resieq  5928  csbima12  6011  dmsnsnsn  6152  csbcog  6229  dfpred3g  6244  predbrg  6254  preddowncl  6265  ordelord  6318  iota5  6456  csbiota  6466  funmoOLD  6494  funimaexgOLD  6565  fconstg  6706  funbrfv  6870  fvelimab  6891  ssimaexg  6904  fvelrn  7004  isoselem  7262  csbriota  7302  csbov123  7371  ovg  7491  caovmo  7563  uniexg  7647  fnse  8033  onfununi  8234  rdg0g  8320  ensn1g  8876  fundmeng  8889  xpdom2g  8925  canth2g  8988  ssfi  9030  php2OLD  9080  canthwdom  9428  zfregcl  9443  elirr  9446  ttrclselem2  9575  tcvalg  9587  tz9.13g  9641  rankvalg  9666  ranklim  9693  r1pwALT  9695  rankuni2b  9702  rankuni  9712  cfslb2n  10117  itunitc1  10269  itunitc  10270  ituniiun  10271  hsmex  10281  axdc2lem  10297  ac7g  10323  ac6sg  10337  numthcor  10343  weth  10344  pwfseqlem4  10511  rankcf  10626  nqereu  10778  prnmax  10844  prlem936  10896  ltord1  11594  xmulasslem  13112  axdc4uz  13797  relexpind  14866  climshft  15376  telfsumo  15605  fsumparts  15609  lcmgcdlem  16400  mreacs  17456  dprdval  19693  fiinopn  22148  neiptoptop  22380  neiptopnei  22381  pt1hmeo  23055  isfildlem  23106  alexsublem  23293  ustuqtop4  23494  voliunlem3  24814  dvbsss  25164  dvfsumlem2  25289  acunirnmpt  31224  acunirnmpt2  31225  acunirnmpt2f  31226  carsgsigalem  32523  carsgclctunlem2  32527  carsgclctun  32529  pmeasmono  32532  pmeasadd  32533  sitgclg  32550  mclsrcl  33763  iota5f  33906  shftvalg  33931  dfrdg2  33998  fvsingle  34313  fullfunfv  34340  ranksng  34560  rankelg  34561  rankpwg  34562  rankeq1o  34564  mblfinlem3  35914  ismrer1  36094  mzpclall  40799  mzpcompact2  40824  diophrw  40831  monotuz  41014  monotoddzz  41016  oddcomabszz  41017  flcidc  41250  nzss  42245  pm14.122b  42351  sbiota1  42362  fiiuncl  42922  axccdom  43078  axccd  43085  monoords  43160  fperiodmullem  43166  0ellimcdiv  43515  cncfperiod  43745  icccncfext  43753  fperdvper  43785  dvnmul  43809  dvnprodlem2  43813  iblspltprt  43839  itgspltprt  43845  stoweidlem4  43870  stoweidlem6  43872  stoweidlem8  43874  stoweidlem15  43881  stoweidlem16  43882  stoweidlem19  43885  stoweidlem20  43886  stoweidlem22  43888  stoweidlem23  43889  stoweidlem27  43893  stoweidlem30  43896  stoweidlem32  43898  stoweidlem34  43900  stoweidlem42  43908  stoweidlem48  43914  fourierdlem11  43984  fourierdlem16  43989  fourierdlem21  43994  fourierdlem41  44014  fourierdlem42  44015  fourierdlem46  44018  fourierdlem48  44020  fourierdlem49  44021  fourierdlem50  44022  fourierdlem68  44040  fourierdlem72  44044  fourierdlem76  44048  fourierdlem79  44051  fourierdlem81  44053  fourierdlem89  44061  fourierdlem90  44062  fourierdlem91  44063  fourierdlem92  44064  fourierdlem97  44069  fourierdlem103  44075  fourierdlem104  44076  fourierdlem111  44083  sge0f1o  44246  sge0p1  44278  hoidmvlelem4  44462  smfpimcclem  44671  funressnmo  44880  aiota0def  44928  csbafv12g  44969  csbaovg  45012  csbafv212g  45051  funressndmafv2rn  45055  funressnbrafv2  45076  funbrafv2  45079