Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclga Structured version   Visualization version   GIF version

Theorem vtoclga 3522
 Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2142 and ax-11 2158. (Revised by Gino Giotto, 20-Aug-2023.)
Hypotheses
Ref Expression
vtoclga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclga.2 (𝑥𝐵𝜑)
Assertion
Ref Expression
vtoclga (𝐴𝐵𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga
StepHypRef Expression
1 eleq1 2877 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
2 vtoclga.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2imbi12d 348 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
4 vtoclga.2 . . 3 (𝑥𝐵𝜑)
53, 4vtoclg 3515 . 2 (𝐴𝐵 → (𝐴𝐵𝜓))
65pm2.43i 52 1 (𝐴𝐵𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  vtocl2ga  3523  vtoclri  3533  disjxiun  5030  wfis3  6162  opabiota  6728  fvmpt3  6756  fvmptss  6764  fnressn  6904  fressnfv  6906  caovord  7347  caovmo  7373  ordunisuc  7537  tfis3  7562  wfr2a  7970  onfununi  7976  smogt  8002  tz7.44-1  8040  tz7.44-2  8041  tz7.44-3  8042  nnacl  8235  nnmcl  8236  nnecl  8237  nnacom  8241  nnaass  8246  nndi  8247  nnmass  8248  nnmsucr  8249  nnmcom  8250  nnmordi  8255  ixpfn  8465  findcard  8756  findcard2  8757  marypha1  8897  cantnfle  9133  cantnflem1  9151  cnfcom  9162  fseqenlem1  9450  nnadju  9623  ackbij1lem8  9653  cardcf  9678  cfsmolem  9696  wunex2  10164  ingru  10241  recrecnq  10393  prlem934  10459  nn1suc  11662  uzind4s2  12314  rpnnen1lem6  12386  cnref1o  12389  xmulasslem  12683  om2uzsuci  13328  expcl2lem  13454  hashpw  13810  seqcoll  13835  climub  15027  climserle  15028  sumrblem  15077  fsumcvg  15078  summolem2a  15081  infcvgaux2i  15222  prodfn0  15259  prodfrec  15260  prodrblem  15292  fprodcvg  15293  prodmolem2a  15297  divalglem8  15758  bezoutlem1  15894  alginv  15926  algcvg  15927  algcvga  15930  algfx  15931  prmind2  16036  prmpwdvds  16247  cnextfvval  22708  xrsxmet  23452  xrhmeo  23589  cmetcaulem  23930  bcth3  23973  itg2addlem  24400  taylfval  24995  sinord  25167  logexprlim  25850  lgsdir2lem4  25953  hlim2  29016  elnlfn  29752  lnconi  29857  chirredlem3  30216  chirredlem4  30217  cnre2csqlem  31326  eulerpartlemsf  31790  eulerpartlemn  31812  bnj1321  32472  bnj1418  32485  subfacp1lem1  32602  frins3  33269  fpr2  33316  frr2  33321  nn0prpwlem  33846  findreccl  33977  mptsnunlem  34822  rdgeqoa  34854  domalom  34888  poimirlem22  35146  poimirlem26  35150  mblfinlem3  35163  mblfinlem4  35164  ismblfin  35165  ftc1anclem3  35199  ftc1anclem8  35204  sdclem2  35247  iscringd  35503  renegclALT  36326  zindbi  39974  fmuldfeq  42309  sumnnodd  42356  iblspltprt  42699  stoweidlem2  42728  stoweidlem17  42743  stoweidlem21  42747  stoweidlem43  42769  stoweidlem51  42777  wallispi  42796
 Copyright terms: Public domain W3C validator