Theorem vtoclga 3533

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2147 and ax-11 2163. (Revised by GG, 20-Aug-2023.)

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		eleq1 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3512	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 52	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  vtocl2ga  3534  vtocl3ga  3539  vtoclri  3545  disjxiun  5096  wfis3  6316  opabiota  6917  fvmpt3  6947  fvmptss  6955  fnressn  7105  fressnfv  7107  caovord  7571  caovmo  7597  ordunisuc  7776  tfis3  7802  fpr2a  8246  frrdmcl  8252  onfununi  8275  smogt  8301  tz7.44-1  8339  tz7.44-2  8340  tz7.44-3  8341  nnacl  8541  nnmcl  8542  nnecl  8543  nnacom  8547  nnaass  8552  nndi  8553  nnmass  8554  nnmsucr  8555  nnmcom  8556  nnmordi  8561  ixpfn  8845  findcard  9092  findcard2  9093  marypha1  9341  cantnfle  9584  cantnflem1  9602  cnfcom  9613  frr2  9676  fseqenlem1  9938  nnadju  10112  ackbij1lem8  10140  cardcf  10166  cfsmolem  10184  wunex2  10653  ingru  10730  recrecnq  10882  prlem934  10948  nn1suc  12171  uzind4s2  12826  rpnnen1lem6  12899  cnref1o  12902  xmulasslem  13204  om2uzsuci  13875  expcl2lem  14000  hashpw  14363  seqcoll  14391  climub  15589  climserle  15590  sumrblem  15638  fsumcvg  15639  summolem2a  15642  infcvgaux2i  15785  prodfn0  15821  prodfrec  15822  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  divalglem8  16331  bezoutlem1  16470  alginv  16506  algcvg  16507  algcvga  16510  algfx  16511  prmind2  16616  prmpwdvds  16836  cnextfvval  24013  xrsxmet  24758  xrhmeo  24904  cmetcaulem  25248  bcth3  25291  itg2addlem  25719  taylfval  26326  sinord  26503  logexprlim  27196  lgsdir2lem4  27299  noseqind  28292  hlim2  31271  elnlfn  32007  lnconi  32112  chirredlem3  32471  chirredlem4  32472  cnre2csqlem  34069  eulerpartlemsf  34518  eulerpartlemn  34540  bnj1321  35185  bnj1418  35198  subfacp1lem1  35375  nn0prpwlem  36518  findreccl  36649  weiunlem  36659  mptsnunlem  37545  rdgeqoa  37577  domalom  37611  poimirlem22  37845  poimirlem26  37849  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  ftc1anclem3  37898  ftc1anclem8  37903  sdclem2  37945  iscringd  38201  renegclALT  39291  zindbi  43255  fmuldfeq  45896  sumnnodd  45943  iblspltprt  46284  stoweidlem2  46313  stoweidlem17  46328  stoweidlem21  46332  stoweidlem43  46354  stoweidlem51  46362  wallispi  46381