Theorem vtoclga 3413

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)

Hypotheses

Ref	Expression
vtoclga.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclga.2	⊢ (𝑥 ∈ 𝐵 → 𝜑)

Assertion

Ref	Expression
vtoclga	⊢ (𝐴 ∈ 𝐵 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga

Step	Hyp	Ref	Expression
1		nfcv 2903	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1993	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 3412	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343

This theorem is referenced by:  vtoclri  3424  ssuniOLD  4613  disjxiun  4802  wfis3  5883  opabiota  6425  fvmpt3  6450  fvmptss  6456  fnressn  6590  fressnfv  6592  caovord  7012  caovmo  7038  ordunisuc  7199  tfis3  7224  wfr2a  7603  onfununi  7609  smogt  7635  tz7.44-1  7673  tz7.44-2  7674  tz7.44-3  7675  nnacl  7863  nnmcl  7864  nnecl  7865  nnacom  7869  nnaass  7874  nndi  7875  nnmass  7876  nnmsucr  7877  nnmcom  7878  nnmordi  7883  ixpfn  8083  findcard  8367  findcard2  8368  marypha1  8508  cantnfle  8744  cantnflem1  8762  cnfcom  8773  fseqenlem1  9058  ackbij1lem5  9259  ackbij1lem8  9262  cardcf  9287  cfsmolem  9305  wunex2  9773  ingru  9850  recrecnq  10002  prlem934  10068  nn1suc  11254  uzind4s2  11963  rpnnen1lem6  12033  rpnnen1OLD  12039  cnref1o  12041  xmulasslem  12329  om2uzsuci  12962  expcl2lem  13087  hashmap  13435  hashpw  13436  seqcoll  13461  climub  14612  climserle  14613  sumrblem  14662  fsumcvg  14663  summolem2a  14666  infcvgaux2i  14810  prodfn0  14846  prodfrec  14847  prodrblem  14879  fprodcvg  14880  prodmolem2a  14884  divalglem8  15346  bezoutlem1  15479  alginv  15511  algcvg  15512  algcvga  15515  algfx  15516  prmind2  15621  prmpwdvds  15831  cnextfvval  22091  xrsxmet  22834  xrhmeo  22967  cmetcaulem  23307  bcth3  23349  itg2addlem  23745  taylfval  24333  sinord  24501  logexprlim  25171  lgsdir2lem4  25274  hlim2  28380  elnlfn  29118  lnconi  29223  chirredlem3  29582  chirredlem4  29583  cnre2csqlem  30287  eulerpartlemsf  30752  eulerpartlemn  30774  bnj1321  31424  bnj1418  31437  subfacp1lem1  31490  frins3  32079  nn0prpwlem  32645  findreccl  32780  mptsnunlem  33515  rdgeqoa  33548  poimirlem22  33763  poimirlem26  33767  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  ftc1anclem3  33819  ftc1anclem8  33824  sdclem2  33870  iscringd  34129  renegclALT  34771  zindbi  38032  fmuldfeq  40337  sumnnodd  40384  iblspltprt  40711  stoweidlem2  40741  stoweidlem17  40756  stoweidlem21  40760  stoweidlem43  40782  stoweidlem51  40790  wallispi  40809